# On global induction mechanisms in a $\mu $-calculus with explicit approximations

RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications (2003)

- Volume: 37, Issue: 4, page 365-391
- ISSN: 0988-3754

## Access Full Article

top## Abstract

top## How to cite

topSprenger, Christoph, and Dam, Mads. "On global induction mechanisms in a $\mu $-calculus with explicit approximations." RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications 37.4 (2003): 365-391. <http://eudml.org/doc/245323>.

@article{Sprenger2003,

abstract = {We investigate a Gentzen-style proof system for the first-order $\mu $-calculus based on cyclic proofs, produced by unfolding fixed point formulas and detecting repeated proof goals. Our system uses explicit ordinal variables and approximations to support a simple semantic induction discharge condition which ensures the well-foundedness of inductive reasoning. As the main result of this paper we propose a new syntactic discharge condition based on traces and establish its equivalence with the semantic condition. We give an automata-theoretic reformulation of this condition which is more suitable for practical proofs. For a detailed comparison with previous work we consider two simpler syntactic conditions and show that they are more restrictive than our new condition.},

author = {Sprenger, Christoph, Dam, Mads},

journal = {RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications},

keywords = {inductive reasoning; circular proofs; well-foundedness; global consistency condition; $\mu $-calculus; approximants},

language = {eng},

number = {4},

pages = {365-391},

publisher = {EDP-Sciences},

title = {On global induction mechanisms in a $\mu $-calculus with explicit approximations},

url = {http://eudml.org/doc/245323},

volume = {37},

year = {2003},

}

TY - JOUR

AU - Sprenger, Christoph

AU - Dam, Mads

TI - On global induction mechanisms in a $\mu $-calculus with explicit approximations

JO - RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications

PY - 2003

PB - EDP-Sciences

VL - 37

IS - 4

SP - 365

EP - 391

AB - We investigate a Gentzen-style proof system for the first-order $\mu $-calculus based on cyclic proofs, produced by unfolding fixed point formulas and detecting repeated proof goals. Our system uses explicit ordinal variables and approximations to support a simple semantic induction discharge condition which ensures the well-foundedness of inductive reasoning. As the main result of this paper we propose a new syntactic discharge condition based on traces and establish its equivalence with the semantic condition. We give an automata-theoretic reformulation of this condition which is more suitable for practical proofs. For a detailed comparison with previous work we consider two simpler syntactic conditions and show that they are more restrictive than our new condition.

LA - eng

KW - inductive reasoning; circular proofs; well-foundedness; global consistency condition; $\mu $-calculus; approximants

UR - http://eudml.org/doc/245323

ER -

## References

top- [1] T. Arts, M. Dam, L. Fredlund and D. Gurov, System description: Verification of distributed Erlang programs. Lecture Notes in Artificial Intelligence 1421 (1998) 38-41.
- [2] J. Bradfield and C. Stirling, Local model checking for infinite state spaces. Theor. Comput. Sci. 96 (1992) 157-174. Zbl0747.68036MR1158715
- [3] M. Dam, Proving properties of dynamic process networks. Inf. Comput. 140 (1998) 95-114. Zbl0892.68034MR1604188
- [4] M. Dam and D. Gurov, $\mu $-calculus with explicit points and approximations. J. Logic Comput. 12 (2002) 43-57. Previously appeared in Fixed Points in Computer Science, FICS (2000). Zbl1003.03033MR1900380
- [5] E.A. Emerson and C.L. Lei, Modalities for model checking: branching time strikes back. Sci. Comput. Program. 8 (1987) 275-306. Zbl0615.68019MR896005
- [6] L. Fredlund, A Framework for Reasoning about Erlang Code. Ph.D. thesis, Royal Institute of Technology, Stockholm, Sweden (2001).
- [7] D. Kozen, Results on the propositional $\mu $-calculus. Theor. Comput. Sci. 27 (1983) 333-354. Zbl0553.03007MR731069
- [8] D. Niwiński and I. Walukiewicz, Games for the $\mu $-calculus. Theor. Comput. Sci. 163 (1997) 99–116. Zbl0872.03017
- [9] D. Park, Finiteness is mu-ineffable. Theor. Comput. Sci. 3 (1976) 173-181. Zbl0353.02027MR437297
- [10] S. Safra, On the complexity of $\omega $-automata, in 29th IEEE Symposium on Foundations of Computer Science (1988) 319-327.
- [11] U. Schöpp, Formal verification of processes. Master’s thesis, University of Edinburgh (2001)
- [12] U. Schöpp and A. Simpson, Verifying temporal properties using explicit approximants: Completeness for context-free processes, in Foundations of Software Science and Computational Structures (FoSSaCS 02), Grenoble, France. Springer, Lecture Notes in Comput. Sci. 2303 (2002) 372-386. Zbl1077.68717MR1965564
- [13] C. Sprenger and M. Dam, On the structure of inductive reasoning: Circular and tree-shaped proofs in the $\mu $-calculus, Foundations of Software Science and Computational Structures (FoSSaCS 03), Warsaw, Poland, April 7–11 2003. A. Gordon, Springer, Lecture Notes in Comput. Sci. 2620 (2003) 425-440. Zbl1029.03016
- [14] C. Stirling and D. Walker, Local model checking in the modal $\mu $-calculus. Theor. Comput. Sci. 89 (1991) 161-177. Zbl0745.03027MR1133710
- [15] W. Thomas, Automata on infinite objects. J. van Leeuwen, Elsevier Science Publishers, Amsterdam, Handb. Theor. Comput. Sci. B (1990) 133-191. Zbl0900.68316MR1127189

## NotesEmbed ?

topTo embed these notes on your page include the following JavaScript code on your page where you want the notes to appear.