Abstract
We study a logic called FLC (Fixpoint Logic with Chop) that extends the modal mu-calculus by a chop-operator and termination formulae. For this purpose formulae are interpreted by predicate transformers instead of predicates. We show that any context-free process can be characterized by an FLC-formula up to bisimulation or simulation. Moreover, we establish the following results: FLC is strictly more expressive than the modal mu-calculus; it is decidable for finite-state processes but undecidable for context-free processes; satisfiability and validity are undecidable; FLC does not have the finite-model property.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
J. A. Bergstra and J. W. Klop. Algebra of communicating processes with abstraction. Theoretical Computer Science, 37:77–121, 1985.
O. Burkart and J. Esparza. More infinite results. ENTCS, 6, 1997. URL: http://www.elsevier.nl/locate/entcs/volume6.html
O. Burkart and B. Steffen. Model checking the full modal mu-calculus for infinite sequential processes. In ICALP’ 97, LNCS 1256, 419–429. Springer-Verlag, 1997.
D. Caucal. On the regular structure of prefix rewriting. Theoretical Computer Science, 106:61–86, 1992.
K. Fisler. Containment of regular languages in non-regular timing diagram languages is decidable. In CAV’97, LNCS 1254. Springer-Verlag, 1997.
J. F. Groote and H. Hüttel. Undecidable equivalences for basic process algebra. Information and Computation, 115(2):354–371, 1994.
J. E. Hopcroft and J. D. Ullman. Introduction to Automata Theory, Languages and Computation. Addison-Wesley, 1979.
D. Kozen. Results on the propositional mu-calculus. Theoretical Computer Science, 27:333–354, 1983.
D. Kozen. A finite model theorem for the propositional mu-calculus. Studia Logica, 47:233–241, 1988.
A. Mader. Modal mu-calculus, model checking and Gauss elimination. In TACAS’95, LNCS 1019, 72–88. Springer-Verlag, 1995.
R. Milner. Communication and Concurrency. Prentice Hall, 1989.
F. Moller. Infinite results. In CONCUR’96, LNCS 1119, 195–216. Springer-Verlag, 1996.
B. Moszkowski. A temporal logic for multi-level reasoning about hardware. IEEE Computer, 18(2):10–19, 1985.
M. Müller-Olm. Derivation of characteristic formulae. ENTCS, 18, 1998. URL: http://www.elsevier.nl/locate/entcs/volume18. html
D. M. R. Park. Concurrency and automata on infinite sequences. In LNCS 154, 561–572. Springer-Verlag, 1981.
B. Steffen and A. Ingólfsdóttir. Characteristic formulae for processes with divergence. Information and Computation, 110(1):149–163, 1994.
Zhou Chaochen, C. A. R. Hoare, and A. P. Ravn. A calculus of durations. Information Processing Letters, 40(5):269–276, 1991.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1999 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Müller-Olm, M. (1999). A Modal Fixpoint Logic with Chop. In: Meinel, C., Tison, S. (eds) STACS 99. STACS 1999. Lecture Notes in Computer Science, vol 1563. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-49116-3_48
Download citation
DOI: https://doi.org/10.1007/3-540-49116-3_48
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-65691-3
Online ISBN: 978-3-540-49116-3
eBook Packages: Springer Book Archive