Title :
On model construction for modal mu-calculus
Author_Institution :
Inst. of Software, Grad. Sch. of Chinese Acad. of Sci., Beijing, China
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;
Conference_Titel :
Theoretical Aspects of Software Engineering (TASE), 2012 Sixth International Symposium on
Conference_Location :
Beijing
Print_ISBN :
978-1-4673-2353-6
DOI :
10.1109/TASE.2012.49
