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

Article

Weak automata for the linear time µ-calculus

Author:

Martin LangeAuthors Info & Claims

VMCAI'05: Proceedings of the 6th international conference on Verification, Model Checking, and Abstract Interpretation

Pages 267 - 281

https://doi.org/10.1007/978-3-540-30579-8_18

Published: 17 January 2005 Publication History

Abstract

This paper presents translations forth and back between formulas of the linear time μ-calculus and finite automata with a weak parity acceptance condition. This yields a normal form for these formulas, in fact showing that the linear time alternation hierarchy collapses at level 0 and not just at level 1 as known so far. The translation from formulas to automata can be optimised yielding automata whose size is only exponential in the alternation depth of the formula.

References

[1]

H. Barringer, R. Kuiper, and A. Pnueli. A really abstract concurrent model and its temporal logic. In Proc. 13th Annual ACM Symp. on Principles of Programming Languages, pages 173-183. ACM, 1986.

Digital Library

[2]

H. Békic. Programming Languages and Their Definition, Selected Papers, volume 177 of LNCS. Springer, 1984.

Digital Library

[3]

A. Biere, A. Cimatti, E. M. Clarke, and Y. Zhu. Symbolic model checking without BDDs. In R. Cleaveland, editor, Proc. 5th Int. Conf. on Tools and Algorithms for the Analysis and Construction of Systems, TACAS'99, volume 1579 of LNCS, Amsterdam, NL, March 1999.

Digital Library

[4]

J. C. Bradfield. The modal µ-calculus alternation hierarchy is strict. In U. Montanari and V. Sassone, editors, Proc. 7th Conf. on Concurrency Theory, CONCUR' 96, volume 1119 of LNCS, pages 233-246, Pisa, Italy, August 1996. Springer.

Digital Library

[5]

J. R. Büchi. On a decision method in restricted second order arithmetic. In Proc. Congress on Logic, Method, and Philosophy of Science, pages 1-12, Stanford, CA, USA, 1962. Stanford University Press.

[6]

A. K. Chandra, D. C. Kozen, and L. J. Stockmeyer. Alternation. Journal of the ACM, 28(1):114-133, January 1981.

Digital Library

[7]

S. Dziembowski, M. Jurdziński, and I. Walukiewicz. How much memory is needed to win infinite games? In Proc. 12th Symp. on Logic in Computer Science, LICS'97, pages 99-110, Warsaw, Poland, June 1997. IEEE.

Digital Library

[8]

E. A. Emerson. Model checking and the µ-calculus. In N. Immerman and P. G. Kolaitis, editors, Descriptive Complexity and Finite Models, volume 31 of DIMACS: Series in Discrete Mathematics and Theoretical Computer Science, chapter 6. AMS, 1997.

[9]

E. A. Emerson and C. S. Jutla. Tree automata, µ-calculus and determinacy. In Proc. 32nd Symp. on Foundations of Computer Science, pages 368-377, San Juan, Puerto Rico, October 1991. IEEE.

Digital Library

[10]

D. Janin and I. Walukiewicz. On the expressive completeness of the propositional µ-calculus with respect to monadic second order logic. In U. Montanari and V. Sassone, editors, Proc. 7th Conf. on Concurrency Theory, CONCUR'96, volume 1119 of LNCS, pages 263-277, Pisa, Italy, August 1996. Springer.

Digital Library

[11]

R. Kaivola. Using Automata to Characterise Fixed Point Temporal Logics. PhD thesis, LFCS, Division of Informatics, The University of Edinburgh, 1997. Tech. Rep. ECS-LFCS-97-356.

[12]

D. Kozen. Results on the propositional µ-calculus. TCS, 27:333-354, December 1983.

[13]

O. Kupferman and M. Y. Vardi. Weak alternating automata are not that weak. ACM Transactions on Computational Logic, 2(3):408-429, 2001.

Digital Library

[14]

O. Kupferman, M. Y. Vardi, and P. Wolper. An automata-theoretic approach to branching-time model checking. Journal of the ACM, 47(2):312-360, March 2000.

Digital Library

[15]

C. Löding and W. Thomas. Alternating automata and logics over infinite words. In Proc. IFIP Int. Conf. on Theoretical Computer Science, IFIP TCS2000, volume 1872 of LNCS, pages 521-535. Springer, August 2000.

Digital Library

[16]

D. Muller and P. Schupp. Alternating automata on infinite objects: determinacy and rabin's theorem. In M. Nivat and D. Perrin, editors, Proc. Ecole de Printemps d'Informatique Théoretique on Automata on Infinite Words, volume 192 of LNCS, pages 100-107, Le Mont Dore, France, May 1984. Springer.

Digital Library

[17]

D. E. Muller, A. Saoudi, and P. E. Schupp. Weak alternating automata give a simple explanation of why most temporal and dynamic logics are decidable in exponential time. In Proc. 3rd Symp. on Logic in Computer Science, LICS'88, pages 422-427, Edinburgh, Scotland, July 1988. IEEE.

[18]

M. O. Rabin. Decidability of second-order theories and automata on infinite trees. Trans. of Amer. Math. Soc., 141:1-35, 1969.

[19]

C. Stirling. Local model checking games. In I. Lee and S. A. Smolka, editors, Proc. 6th Conf. on Concurrency Theory, CONCUR'95, volume 962 of LNCS, pages 1-11, Berlin, Germany, August 1995. Springer.

Digital Library

[20]

M. Y. Vardi. A temporal fixpoint calculus. In ACM, editor, Proc. Conf. on Principles of Programming Languages, POPL'88, pages 250-259, NY, USA, 1988. ACM Press.

Digital Library

[21]

M. Y. Vardi. An Automata-Theoretic Approach to Linear Temporal Logic, volume 1043 of LNCS, pages 238-266. Springer, New York, NY, USA, 1996.

Digital Library

[22]

I. Walukiewicz. Completeness of Kozen's axiomatization of the propositional µ-calculus. In Proc. 10th Symp. on Logic in Computer Science, LICS'95, pages 14-24, Los Alamitos, CA, 1995. IEEE.

Digital Library

Cited By

Lakenbrink RMüller-Olm MOhrem CGutsfeld J(2024)A Navigation Logic for Recursive Programs with Dynamic Thread CreationVerification, Model Checking, and Abstract Interpretation10.1007/978-3-031-50521-8_3(48-70)Online publication date: 15-Jan-2024
https://dl.acm.org/doi/10.1007/978-3-031-50521-8_3
Gutsfeld JMüller-Olm MOhrem C(2021)Automata and fixpoints for asynchronous hyperpropertiesProceedings of the ACM on Programming Languages10.1145/34343195:POPL(1-29)Online publication date: 4-Jan-2021
https://dl.acm.org/doi/10.1145/3434319
Aceto LAchilleos AFrancalanza AIngólfsdóttir ALehtinen K(2019)Adventures in monitorability: from branching to linear time and back againProceedings of the ACM on Programming Languages10.1145/32903653:POPL(1-29)Online publication date: 2-Jan-2019
https://dl.acm.org/doi/10.1145/3290365
Show More Cited By

Weak automata for the linear time µ-calculus
1. Theory of computation
  1. Logic

Recommendations

Weak alternating automata are not that weak

Automata on infinite words are used for specification and verification of nonterminating programs. Different types of automata induce different levels of expressive power, of succinctness, and of complexity. Alternating automata have both existential and ...
Enriched µ-calculus pushdown module checking
LPAR'07: Proceedings of the 14th international conference on Logic for programming, artificial intelligence and reasoning

The model checking problem for open systems (called module checking) has been intensively studied in the literature, both for finite-state and infinite-state systems. In this paper, we focus on pushdown module checking with respect to µ-calculus ...
Alternating automata and a temporal fixpoint calculus for visibly pushdown languages
CONCUR'07: Proceedings of the 18th international conference on Concurrency Theory

We investigate various classes of alternating automata for visibly pushdown languages (VPL) over infinite words. First, we show that alternating visibly pushdown automata (AVPA) are exactly as expressive as their nondeterministic counterpart (NVPA) but ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

VMCAI'05: Proceedings of the 6th international conference on Verification, Model Checking, and Abstract Interpretation

January 2005

481 pages

ISBN:354024297X

Editor:
Radhia Cousot
CNRS, Paris, France

Sponsors

ACM: Association for Computing Machinery
EAPLS: European Association for Programming Languages and Systems

Publisher

Springer-Verlag

Berlin, Heidelberg

Publication History

Published: 17 January 2005

Check for updates

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

7
Total Citations
View Citations
0
Total Downloads

Downloads (Last 12 months)0
Downloads (Last 6 weeks)0

Reflects downloads up to 13 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

Lakenbrink RMüller-Olm MOhrem CGutsfeld J(2024)A Navigation Logic for Recursive Programs with Dynamic Thread CreationVerification, Model Checking, and Abstract Interpretation10.1007/978-3-031-50521-8_3(48-70)Online publication date: 15-Jan-2024
https://dl.acm.org/doi/10.1007/978-3-031-50521-8_3
Gutsfeld JMüller-Olm MOhrem C(2021)Automata and fixpoints for asynchronous hyperpropertiesProceedings of the ACM on Programming Languages10.1145/34343195:POPL(1-29)Online publication date: 4-Jan-2021
https://dl.acm.org/doi/10.1145/3434319
Aceto LAchilleos AFrancalanza AIngólfsdóttir ALehtinen K(2019)Adventures in monitorability: from branching to linear time and back againProceedings of the ACM on Programming Languages10.1145/32903653:POPL(1-29)Online publication date: 2-Jan-2019
https://dl.acm.org/doi/10.1145/3290365
Genevès PLayaïda NSchmitt AGesbert N(2015)Efficiently Deciding μ-Calculus with Converse over Finite TreesACM Transactions on Computational Logic10.1145/272471216:2(1-41)Online publication date: 2-Apr-2015
https://dl.acm.org/doi/10.1145/2724712
Sánchez CLeucker M(2010)Regular linear temporal logic with pastProceedings of the 11th international conference on Verification, Model Checking, and Abstract Interpretation10.1007/978-3-642-11319-2_22(295-311)Online publication date: 17-Jan-2010
https://dl.acm.org/doi/10.1007/978-3-642-11319-2_22
Leucker MSánchez C(2007)Regular linear temporal logicProceedings of the 4th international conference on Theoretical aspects of computing10.5555/1777259.1777279(291-305)Online publication date: 26-Sep-2007
https://dl.acm.org/doi/10.5555/1777259.1777279
Jehle MJohannsen JLange MRachinsky N(2006)Bounded Model Checking for All Regular PropertiesElectronic Notes in Theoretical Computer Science (ENTCS)10.1016/j.entcs.2005.07.016144:1(3-18)Online publication date: 1-Jan-2006
https://dl.acm.org/doi/10.1016/j.entcs.2005.07.016

View Options

View options

Media

Figures

Other

Tables

View Table of Contents