A decidable mu-calculus: Preliminary report
- 1 October 1981
- conference paper
- Published by Institute of Electrical and Electronics Engineers (IEEE)
- No. 02725428,p. 421-427
- https://doi.org/10.1109/sfcs.1981.4
Abstract
We describe a mu-calculus which amounts to modal logic plus a minimization operator, and show that its satisfiability problem is decidable in exponential time. This result subsumes corresponding results for propositional dynamic logic with test and converse, thus supplying a better setting for those results. It also encompasses similar results for a logic of flowgraphs. This work provides an intimate link between PDL as defined by the Segerberg axioms and the mu-calculi of de Bakker and Park.Keywords
This publication has 9 references indexed in Scilit:
- Modal logic of concurrent nondeterministic programsPublished by Springer Nature ,2005
- Dynamic algebras and the nature of inductionPublished by Association for Computing Machinery (ACM) ,1980
- Models of program logicsPublished by Institute of Electrical and Electronics Engineers (IEEE) ,1979
- Propositional dynamic logic of regular programsJournal of Computer and System Sciences, 1979
- Complexity of expressions allowing concurrencyPublished by Association for Computing Machinery (ACM) ,1978
- The temporal logic of programsPublished by Institute of Electrical and Electronics Engineers (IEEE) ,1977
- Finiteness is mu-ineffableTheoretical Computer Science, 1976
- Complexity measures for regular expressionsJournal of Computer and System Sciences, 1976
- Consistent and complementary formal theories of the semantics of programming languagesActa Informatica, 1974