More Web Proxy on the site http://driver.im/

research-article

Towards Completeness via Proof Search in the Linear Time μ-calculus: The case of Büchi inclusions

Authors:

Alexis SaurinAuthors Info & Claims

LICS '16: Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science

Pages 377 - 386

https://doi.org/10.1145/2933575.2933598

Published: 05 July 2016 Publication History

Abstract

Modal μ-calculus is one of the central languages of logic and verification, whose study involves notoriously complex objects: automata over infinite structures on the model-theoretical side; infinite proofs and proofs by (co)induction on the proof-theoretical side. Nevertheless, axiomatizations have been given for both linear and branching time μ-calculi, with quite involved completeness arguments. We come back to this central problem, considering it from a proof search viewpoint, and provide some new completeness arguments in the linear time μ-calculus. Our results only deal with restricted classes of formulas that closely correspond to (non-alternating) ω-automata but, compared to earlier proofs, our completeness arguments are direct and constructive. We first consider a natural circular proof system based on sequent calculus, and show that it is complete for inclusions of parity automata expressed as formulas, making use of Safra's construction directly in proof search. We then consider the corresponding finitary proof system, featuring (co)induction rules, and provide a partial translation result from circular to finitary proofs. This yields completeness of the finitary proof system for inclusions of sufficiently deterministic parity automata, and finally for arbitrary Büchi automata.

References

[1]

D. Baelde. Least and greatest fixed points in linear logic. ACM Transactions on Computational Logic (TOCL), 13(1):2, 2012.

Digital Library

[2]

J. C. Bradfield, J. Esparza, and A. Mader. An effective tableau system for the linear time μ-calculus. In F. M. auf der Heide and B. Monien, editors, ICALP 96, volume 1099 of LNCS, pages 98--109. Springer, 1996. ISBN 3-540-61440-0. 120.

Digital Library

[3]

J. Brotherston and N. Gorogiannis. Cyclic abduction of inductively defined safety and termination preconditions. In M. Müller-Olm and H. Seidl, editors, SAS 2014. Proceedings, volume 8723 of LNCS, pages 68--84. Springer, 2014. ISBN 978-3-319-10935-0.

[4]

J. Brotherston and A. Simpson. Sequent calculi for induction and infinite descent. Journal of Logic and Computation 21(6):1177--1216, 2011.

Digital Library

[5]

Z. Chihani, D. Miller, and F. Renaud. Foundational proof certificates in first-order logic. In Automated Deduction--CADE-24, pages 162--177. Springer, 2013.

Digital Library

[6]

C. Dax, M. Hofmann, and M. Lange. A proof system for the linear time μ-calculus. In S. Arun-Kumar and N. Garg, editors, FSTTCS'06, volume 4337 of LNCS, pages 273--284. Springer, 2006. ISBN 3-540-49994-6. 26.

Digital Library

[7]

A. Doumane, D. Baelde, L. Hirschi, and A. Saurin. Towards completeness via proof search in the linear time μ-calculus (extended version). https://hal.archives-ouvertes.fr/hal-01275289.

Digital Library

[8]

J. Fortier and L. Santocanale. Cuts for circular proofs: semantics and cut-elimination. In S. R. D. Rocca, editor, CSL'13, volume 23 of LIPIcs, pages 248--262. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2013. ISBN 978-3-939897-60-6.

[9]

E. Grädel, W. Thomas, and T. Wilke, editors. Automata Logics, and Infinite Games: A Guide to Current Research. Springer-Verlag New York, Inc., New York, NY, USA, 2002. ISBN 3-540-00388-6.

[10]

D. Janin and I. Walukiewicz. Automata for the modal mu-calculus and related results. In J. Wiedermann and P. Hájek, editors, MFCS'95, volume 969 of LNCS, pages 552--562. Springer, 1995. ISBN 3-540-60246-1. 160.

Digital Library

[11]

D. Kähler and T. Wilke. Complementation, disambiguation, and determinization of Büchi automata unified. In ICALP'08, pages 724--735. Springer, 2008.

Digital Library

[12]

R. Kaivola. Axiomatising linear time mu-calculus. In I. Lee and S. A. Smolka, editors, CONCUR'95, Proceedings, volume 962 of LNCS, pages 423--437. Springer, 1995. ISBN 3-540-60218-6. 32.

Digital Library

[13]

D. Kozen. Results on the propositional mu-calculus. Theoretical Computer Science, 27:333--354, 1983.

[14]

D. Miller. A proposal for broad spectrum proof certificates. In Certified Programs and Proofs, pages 54--69. Springer, 2011.

Digital Library

[15]

N. Piterman. From nondeterministic Büchi and Streett automata to deterministic parity automata. Logical Methods in Computer Science, 3(3), 2007.

Digital Library

[16]

S. Safra. Exponential determinization for ω-automata with strong-fairness acceptance condition (extended abstract). In STOC'92, pages 275--282, 1992. ACM. ISBN 0-89791-511-9.

Digital Library

[17]

L. Santocanale. A calculus of circular proofs and its categorical semantics. Technical Report RS-01-15, BRICS, Department of Computer Science, University of Aarhus, May 2001.

[18]

L. Santocanale. A calculus of circular proofs and its categorical semantics. In M. Nielsen and U. Engberg, editors, FOSSACS'02, volume 2303 of LNCS, pages 357--371. Springer, 2002. ISBN 3-540-43366-X.

Digital Library

[19]

C. Stirling and D. Walker. Local model checking in the modal mu-calculus. Theoretical Computer Science, 89(1):161--177, 1991.

Digital Library

[20]

R. S. Streett and E. A. Emerson. An automata theoretic decision procedure for the propositional mu-calculus. Information and Computation, 81(3): 249--264, 1989.

Digital Library

[21]

I. Walukiewicz. On completeness of the mu-calculus. In LICS'93, pages 136--146, 1993.

[22]

I. Walukiewicz. Completeness of Kozen's axiomatisation of the propositional mu-calculus. In LICS'95, pages 14--24. IEEE Computer Society, 1995. ISBN 0-8186-7050-9.

Digital Library

[23]

I. Walukiewicz. Completeness of Kozen's axiomatisation of the propositional mu-calculus. Information and Computation, 157(1-2):142--182, 2000.

Digital Library

Cited By

Baelde DDoumane AKuperberg DSaurin A(2022)Bouncing Threads for Circular and Non-Wellfounded ProofsProceedings of the 37th Annual ACM/IEEE Symposium on Logic in Computer Science10.1145/3531130.3533375(1-13)Online publication date: 2-Aug-2022
https://dl.acm.org/doi/10.1145/3531130.3533375
Cohen L(2021)Non-well-founded Deduction for Induction and CoinductionAutomated Deduction – CADE 2810.1007/978-3-030-79876-5_1(3-24)Online publication date: 5-Jul-2021
https://doi.org/10.1007/978-3-030-79876-5_1
De ASaurin A(2019)Infinets: The Parallel Syntax for Non-wellfounded Proof-TheoryAutomated Reasoning with Analytic Tableaux and Related Methods10.1007/978-3-030-29026-9_17(297-316)Online publication date: 14-Aug-2019
https://doi.org/10.1007/978-3-030-29026-9_17
Show More Cited By

Towards Completeness via Proof Search in the Linear Time μ-calculus: The case of Büchi inclusions
1. Computing methodologies
  1. Symbolic and algebraic manipulation
    1. Symbolic and algebraic algorithms
2. Theory of computation
  1. Logic
  2. Semantics and reasoning

Recommendations

A sequent calculus for type theory
CSL'06: Proceedings of the 20th international conference on Computer Science Logic

Based on natural deduction, Pure Type Systems (PTS) can express a wide range of type theories. In order to express proof-search in such theories, we introduce the Pure Type Sequent Calculi (PTSC) by enriching a sequent calculus due to Herbelin, adapted ...
Constructive linear-time temporal logic: Proof systems and Kripke semantics

In this paper we study a version of constructive linear-time temporal logic (LTL) with the ''next'' temporal operator. The logic is originally due to Davies, who has shown that the proof system of the logic corresponds to a type system for binding-time ...
A Paraconsistent Linear-time Temporal Logic

Inconsistency-tolerant reasoning and paraconsistent logic are of growing importance not only in Knowledge Representation, AI and other areas of Computer Science, but also in Philosophical Logic. In this paper, a new logic, paraconsistent linear-time ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

LICS '16: Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science

July 2016

901 pages

ISBN:9781450343916

DOI:10.1145/2933575

Conference Chair:
Eric Koskinen,
General Chair:
Martin Grohe,
Program Chair:
Natarajan Shankar

Copyright © 2016 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than the author(s) must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected].

Sponsors

SIGLOG: ACM Special Interest Group on Logic and Computation
EACSL: European Association for Computer Science Logic
IEEE-CS\DATC: IEEE Computer Society

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 05 July 2016

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article
Research
Refereed limited

Conference

LICS '16

Sponsor:

SIGLOG
EACSL
IEEE-CS\DATC

LICS '16: 31st Annual ACM/IEEE Symposium on Logic in Computer Science

July 5 - 8, 2016

NY, New York, USA

Acceptance Rates

Overall Acceptance Rate 215 of 622 submissions, 35%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

7
Total Citations
View Citations
56
Total Downloads

Downloads (Last 12 months)3
Downloads (Last 6 weeks)1

Reflects downloads up to 10 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

Baelde DDoumane AKuperberg DSaurin A(2022)Bouncing Threads for Circular and Non-Wellfounded ProofsProceedings of the 37th Annual ACM/IEEE Symposium on Logic in Computer Science10.1145/3531130.3533375(1-13)Online publication date: 2-Aug-2022
https://dl.acm.org/doi/10.1145/3531130.3533375
Cohen L(2021)Non-well-founded Deduction for Induction and CoinductionAutomated Deduction – CADE 2810.1007/978-3-030-79876-5_1(3-24)Online publication date: 5-Jul-2021
https://doi.org/10.1007/978-3-030-79876-5_1
De ASaurin A(2019)Infinets: The Parallel Syntax for Non-wellfounded Proof-TheoryAutomated Reasoning with Analytic Tableaux and Related Methods10.1007/978-3-030-29026-9_17(297-316)Online publication date: 14-Aug-2019
https://doi.org/10.1007/978-3-030-29026-9_17
Doumane AAceto LIngólfsdóttir A(2017)Constructive completeness for the linear-time μ-calculusProceedings of the 32nd Annual ACM/IEEE Symposium on Logic in Computer Science10.5555/3329995.3330010(1-12)Online publication date: 20-Jun-2017
https://dl.acm.org/doi/10.5555/3329995.3330010
Doumane A(2017)Constructive completeness for the linear-time μ-calculus2017 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)10.1109/LICS.2017.8005075(1-12)Online publication date: Jun-2017
https://doi.org/10.1109/LICS.2017.8005075
Das APous D(2017)A Cut-Free Cyclic Proof System for Kleene AlgebraAutomated Reasoning with Analytic Tableaux and Related Methods10.1007/978-3-319-66902-1_16(261-277)Online publication date: 30-Aug-2017
https://doi.org/10.1007/978-3-319-66902-1_16
Doumane ABaelde DHirschi LSaurin AKoskinen EGrohe MShankar N(2016)Towards Completeness via Proof Search in the Linear Time μ-calculusProceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science10.1145/2933575.2933598(377-386)Online publication date: 5-Jul-2016
https://dl.acm.org/doi/10.1145/2933575.2933598

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Table of Contents