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

Sprenger, Christoph; Dam, Mads

doi:10.1051/ita:2003024

On global induction mechanisms in a

μ

-calculus with explicit approximations

Sprenger, Christoph ; Dam, Mads

RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications, Tome 37 (2003) no. 4, pp. 365-391.

Résumé

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.

MR Zbl

DOI : 10.1051/ita:2003024

Classification : 68Q60, 03F07, 03B35
Mots-clés : inductive reasoning, circular proofs, well-foundedness, global consistency condition,

μ

-calculus, approximants

@article{ITA_2003__37_4_365_0,
     author = {Sprenger, Christoph and Dam, Mads},
     title = {On global induction mechanisms in a $\mu $-calculus with explicit approximations},
     journal = {RAIRO - Theoretical Informatics and Applications - Informatique Th\'eorique et Applications},
     pages = {365--391},
     publisher = {EDP-Sciences},
     volume = {37},
     number = {4},
     year = {2003},
     doi = {10.1051/ita:2003024},
     mrnumber = {2053032},
     zbl = {1111.68518},
     language = {en},
     url = {https://www.numdam.org/articles/10.1051/ita:2003024/}
}

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
SP  - 365
EP  - 391
VL  - 37
IS  - 4
PB  - EDP-Sciences
UR  - https://www.numdam.org/articles/10.1051/ita:2003024/
DO  - 10.1051/ita:2003024
LA  - en
ID  - ITA_2003__37_4_365_0
ER  -

%0 Journal Article
%A Sprenger, Christoph
%A Dam, Mads
%T On global induction mechanisms in a $\mu $-calculus with explicit approximations
%J RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications
%D 2003
%P 365-391
%V 37
%N 4
%I EDP-Sciences
%U https://www.numdam.org/articles/10.1051/ita:2003024/
%R 10.1051/ita:2003024
%G en
%F ITA_2003__37_4_365_0

Sprenger, Christoph; Dam, Mads. On global induction mechanisms in a $\mu $-calculus with explicit approximations. RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications, Tome 37 (2003) no. 4, pp. 365-391. doi : 10.1051/ita:2003024. https://www.numdam.org/articles/10.1051/ita:2003024/

Bibliographie
Cité par

[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. | MR | Zbl

[3] M. Dam, Proving properties of dynamic process networks. Inf. Comput. 140 (1998) 95-114. | MR | Zbl

[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). | MR | Zbl

[5] E.A. Emerson and C.L. Lei, Modalities for model checking: branching time strikes back. Sci. Comput. Program. 8 (1987) 275-306. | MR | Zbl

[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 $μ$ -calculus. Theor. Comput. Sci. 27 (1983) 333-354. | MR | Zbl

[8] D. Niwiński and I. Walukiewicz, Games for the $μ$ -calculus. Theor. Comput. Sci. 163 (1997) 99-116. | Zbl

[9] D. Park, Finiteness is mu-ineffable. Theor. Comput. Sci. 3 (1976) 173-181. | MR | Zbl

[10] S. Safra, On the complexity of $ω$ -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. | MR | Zbl

[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. | Zbl

[14] C. Stirling and D. Walker, Local model checking in the modal $μ$ -calculus. Theor. Comput. Sci. 89 (1991) 161-177. | MR | Zbl

[15] W. Thomas, Automata on infinite objects. J. van Leeuwen, Elsevier Science Publishers, Amsterdam, Handb. Theor. Comput. Sci. B (1990) 133-191. | MR | Zbl

Leigh, Graham E.; Wehr, Dominik From GTC to : Generating reset proof systems from cyclic proof systems, Annals of Pure and Applied Logic, Volume 175 (2024) no. 10, p. 103485 | DOI:10.1016/j.apal.2024.103485
Afshari, Bahareh; Wehr, Dominik Abstract cyclic proofs, Mathematical Structures in Computer Science, Volume 34 (2024) no. 7, p. 552 | DOI:10.1017/s0960129524000070
AFSHARI, BAHAREH; ENQVIST, SEBASTIAN; LEIGH, GRAHAM E.; MARTI, JOHANNES; VENEMA, YDE PROOF SYSTEMS FOR TWO-WAY MODAL MU-CALCULUS, The Journal of Symbolic Logic (2023), p. 1 | DOI:10.1017/jsl.2023.60
Simpson, Alex Cyclic Arithmetic Is Equivalent to Peano Arithmetic, Foundations of Software Science and Computation Structures, Volume 10203 (2017), p. 283 | DOI:10.1007/978-3-662-54458-7_17
Brotherston, James; Gorogiannis, Nikos; Petersen, Rasmus L. A Generic Cyclic Theorem Prover, Programming Languages and Systems, Volume 7705 (2012), p. 350 | DOI:10.1007/978-3-642-35182-2_25
Brotherston, J.; Simpson, A. Sequent calculi for induction and infinite descent, Journal of Logic and Computation, Volume 21 (2011) no. 6, p. 1177 | DOI:10.1093/logcom/exq052
Brotherston, James; Simpson, Alex, 22nd Annual IEEE Symposium on Logic in Computer Science (LICS 2007) (2007), p. 51 | DOI:10.1109/lics.2007.16
Brotherston, James Formalised Inductive Reasoning in the Logic of Bunched Implications, Static Analysis, Volume 4634 (2007), p. 87 | DOI:10.1007/978-3-540-74061-2_6
Brotherston, James Cyclic Proofs for First-Order Logic with Inductive Definitions, Automated Reasoning with Analytic Tableaux and Related Methods, Volume 3702 (2005), p. 78 | DOI:10.1007/11554554_8

Cité par 9 documents. Sources : Crossref