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

Christoph Sprenger; Mads Dam

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

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

Abstract

top
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.

How to cite

top

Sprenger, 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. [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. [2] J. Bradfield and C. Stirling, Local model checking for infinite state spaces. Theor. Comput. Sci. 96 (1992) 157-174. Zbl0747.68036MR1158715
  3. [3] M. Dam, Proving properties of dynamic process networks. Inf. Comput. 140 (1998) 95-114. Zbl0892.68034MR1604188
  4. [4] 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). Zbl1003.03033MR1900380
  5. [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. [6] L. Fredlund, A Framework for Reasoning about Erlang Code. Ph.D. thesis, Royal Institute of Technology, Stockholm, Sweden (2001). 
  7. [7] D. Kozen, Results on the propositional μ -calculus. Theor. Comput. Sci. 27 (1983) 333-354. Zbl0553.03007MR731069
  8. [8] D. Niwiński and I. Walukiewicz, Games for the μ -calculus. Theor. Comput. Sci. 163 (1997) 99–116. Zbl0872.03017
  9. [9] D. Park, Finiteness is mu-ineffable. Theor. Comput. Sci. 3 (1976) 173-181. Zbl0353.02027MR437297
  10. [10] S. Safra, On the complexity of ω -automata, in 29th IEEE Symposium on Foundations of Computer Science (1988) 319-327. 
  11. [11] U. Schöpp, Formal verification of processes. Master’s thesis, University of Edinburgh (2001) 
  12. [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. [13] 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
  14. [14] C. Stirling and D. Walker, Local model checking in the modal μ -calculus. Theor. Comput. Sci. 89 (1991) 161-177. Zbl0745.03027MR1133710
  15. [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 ?

top

You 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.

Only the controls for the widget will be shown in your chosen language. Notes will be shown in their authored language.

Tells the widget how many notes to show per page. You can cycle through additional notes using the next and previous controls.

    
                

                
Note: Best practice suggests putting the JavaScript code just before the closing </body> tag.