• DocumentCode
    2984747
  • Title

    On model construction for modal mu-calculus

  • Author

    Qu, Nan

  • Author_Institution
    Inst. of Software, Grad. Sch. of Chinese Acad. of Sci., Beijing, China
  • fYear
    2012
  • fDate
    4-6 July 2012
  • Firstpage
    257
  • Lastpage
    260
  • Abstract
    This paper presents a tableau system for checking satisfiability of modal μ-calculus formulas. When a formula F is satisfiable, a model with size bounded by 2[F] can be extracted from the tableau. We also show that the asymptotic lower bound for the model size of formulas is greater than any polynomial function of the size of formulas.
  • Keywords
    computability; polynomials; process algebra; modal μ-calculus formulas; modal mu-calculus; model construction; polynomial function; satisfiability; tableau system; Computational modeling; Cost accounting; Educational institutions; Polynomials; Radiation detectors; Semantics; Syntactics; µ-calculus; model size; satisfiability; tableau;
  • fLanguage
    English
  • Publisher
    ieee
  • Conference_Titel
    Theoretical Aspects of Software Engineering (TASE), 2012 Sixth International Symposium on
  • Conference_Location
    Beijing
  • Print_ISBN
    978-1-4673-2353-6
  • Type

    conf

  • DOI
    10.1109/TASE.2012.49
  • Filename
    6269656
    • Link To Document
    https://search.isc.ac/dl/search/defaultta.aspx?DTC=49&DC=2984747