# On global induction mechanisms in a μ-calculus with explicit approximations

RAIRO - Theoretical Informatics and Applications (2010)

- 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 μ-calculus with explicit approximations." RAIRO - Theoretical Informatics and Applications 37.4 (2010): 365-391. <http://eudml.org/doc/92728>.

@article{Sprenger2010,

abstract = {
We investigate a Gentzen-style proof system for the first-order μ-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},

keywords = {Inductive reasoning; circular proofs; well-foundedness; global consistency condition; μ-calculus; approximants.; inductive reasoning},

language = {eng},

month = {3},

number = {4},

pages = {365-391},

publisher = {EDP Sciences},

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

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

volume = {37},

year = {2010},

}

TY - JOUR

AU - Sprenger, Christoph

AU - Dam, Mads

TI - On global induction mechanisms in a μ-calculus with explicit approximations

JO - RAIRO - Theoretical Informatics and Applications

DA - 2010/3//

PB - EDP Sciences

VL - 37

IS - 4

SP - 365

EP - 391

AB -
We investigate a Gentzen-style proof system for the first-order μ-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; μ-calculus; approximants.; inductive reasoning

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

ER -

## References

top- T. Arts, M. Dam, L. Fredlund and D. Gurov, System description: Verification of distributed Erlang programs. Lecture Notes in Artificial Intelligence1421 (1998) 38-41.
- J. Bradfield and C. Stirling, Local model checking for infinite state spaces. Theor. Comput. Sci.96 (1992) 157-174 . Zbl0747.68036
- M. Dam, Proving properties of dynamic process networks. Inf. Comput.140 (1998) 95-114. Zbl0892.68034
- M. Dam and D. Gurov, μ-calculus with explicit points and approximations. J. Logic Comput.12 (2002) 43-57. Previously appeared in Fixed Points in Computer Science, FICS (2000).
- E.A. Emerson and C.L. Lei, Modalities for model checking: branching time strikes back. Sci. Comput. Program.8 (1987) 275-306 . Zbl0615.68019
- L. Fredlund, A Framework for Reasoning about Erlang Code. Ph.D. thesis, Royal Institute of Technology, Stockholm, Sweden (2001).
- D. Kozen, Results on the propositional μ-calculus. Theor. Comput. Sci.27 (1983) 333-354 . Zbl0553.03007
- D. Niwinski and I. Walukiewicz, Games for the μ-calculus. Theor. Comput. Sci.163 (1997) 99-116. Zbl0872.03017
- D. Park, Finiteness is mu-ineffable. Theor. Comput. Sci.3 (1976) 173-181 . Zbl0353.02027
- S. Safra, On the complexity of ω-automata, in 29th IEEE Symposium on Foundations of Computer Science (1988) 319-327.
- U. Schöpp, Formal verification of processes. Master's thesis, University of Edinburgh (2001)
- 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.68717
- C. Sprenger and M. Dam, On the structure of inductive reasoning: Circular and tree-shaped proofs in the μ-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
- C. Stirling and D. Walker, Local model checking in the modal -calculus. Theor. Comput. Sci.89 (1991) 161-177 . Zbl0745.03027
- W. Thomas, Automata on infinite objects. J. van Leeuwen, Elsevier Science Publishers, Amsterdam, Handb. Theor. Comput. Sci.B (1990) 133-191. Zbl0900.68316

## NotesEmbed ?

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