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
topHow 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 .
- M. Dam, Proving properties of dynamic process networks. Inf. Comput.140 (1998) 95-114.
- 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 .
- 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 .
- D. Niwinski and I. Walukiewicz, Games for the μ-calculus. Theor. Comput. Sci.163 (1997) 99-116.
- D. Park, Finiteness is mu-ineffable. Theor. Comput. Sci.3 (1976) 173-181 .
- 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.
- 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.
- C. Stirling and D. Walker, Local model checking in the modal -calculus. Theor. Comput. Sci.89 (1991) 161-177 .
- W. Thomas, Automata on infinite objects. J. van Leeuwen, Elsevier Science Publishers, Amsterdam, Handb. Theor. Comput. Sci.B (1990) 133-191.
NotesEmbed ?
topYou must be logged in to post comments.
To embed these notes on your page include the following JavaScript code on your page where you want the notes to appear.