Skip to main content
Disciplines
Automotive Business IT + Informatics Construction + Real Estate Electrical Engineering + Electronics Energy + Sustainability Insurance + Risk Finance + Banking Management + Leadership Marketing + Sales Mechanical Engineering + Materials
Events
DE
EN
Books
Journals
Topic Page
Marketing
Start single access now
Access for companies
EXTENDED SEARCH
Log in
Top
Published in:
Minimal and Monotone Minimal Perfect Hash Functions Read chapter Read first chapter

2015 | OriginalPaper | Chapter

Relating Paths in Transition Systems: The Fall of the Modal Mu-Calculus

Authors : Cătălin Dima, Bastien Maubert, Sophie Pinchinat

Published in: Mathematical Foundations of Computer Science 2015

Publisher: Springer Berlin Heidelberg

Log in

Activate our intelligent search to find suitable subject content or patents.

search-config
loading …

Abstract

We revisit Janin and Walukiewicz’s classic result on the expressive completeness of the modal mu-calculus w.r.t. MSO, when transition systems are equipped with a binary relation over paths. We obtain two natural extensions of MSO and the mu-calculus: MSO with path relation and the jumping mu-calculus. While “bounded-memory” binary relations bring about no extra expressivity to either of the two logics, “unbounded-memory” binary relations make the bisimulation-invariant fragment of MSO with path relation more expressive than the jumping mu-calculus: the existence of winning strategies in games with imperfect-information inhabits the gap.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

inform now
previous chapter Classes of Languages Generated by the Kleene Star of a Word
next chapter Weighted Automata and Logics on Graphs
Footnotes
1
i.e. finite sequences of states and actions that start in the initial state and follow the binary relations.
 
2
The notion of “associated state” is only used to define unfoldings and is left informal.
 
3
i.e. it progresses at the same pace on each tape.
 
4
i.e. has a winning strategy.
 
5
a one-state transducer that accepts it can easily be exhibited.
 
Literature
1.
Alur, R., Černý, P., Chaudhuri, S.: Model checking on trees with path equivalences. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol. 4424, pp. 664–678. Springer, Heidelberg (2007) CrossRef
2.
Apt, K.R., Grädel, E.: Lectures in Game Theory for Computer Scientists. Cambridge University Press, Cambridge (2011)CrossRefMATH
3.
4.
Berwanger, D., Chatterjee, K., De Wulf, M., Doyen, L., Henzinger, T.A.: Strategy construction for parity games with imperfect information. Inf. Comput. 208(10), 1206–1220 (2010)CrossRefMATH
5.
6.
Berwanger, D., Mathew, A.B.: Games with recurring certainty. In: Proceedings of SR Games with Recurring Certainty 2014, pp. 91–96 (2014)
7.
Bozianu, R., Dima, C., Enea, C.: Model checking an epistemic mu-calculus with synchronous and perfect recall semantics. In: TARK 2013 (2013)
8.
9.
Chatterjee, K., Doyen, L.: The complexity of partial-observation parity games. In: Fermüller, C.G., Voronkov, A. (eds.) LPAR-17. LNCS, vol. 6397, pp. 1–14. Springer, Heidelberg (2010) CrossRef
10.
Courcelle, B., Engelfriet, J.: Graph Structure and Monadic Second-Order Logic - A Language-Theoretic Approach. Cambridge University Press, Cambridge (2012)CrossRefMATH
11.
Elgot, C.C., Rabin, M.O.: Decidability and undecidability of extensions of second (first) order theory of (generalized) successor. J. Symb. Log. 31(2), 169–181 (1966)CrossRefMATH
12.
Fagin, R., Halpern, J., Moses, Y., Vardi, M.: Reasoning about knowledge. The MIT Press, Boston (2004)
13.
Grädel, E.: Model-checking games for logics of imperfect information. Theor. Comput. Sci. 493, 2–14 (2013)CrossRefMATH
14.
Farwer, B.: 1 omega-Automata. In: Grädel, E., Thomas, W., Wilke, T. (eds.) Automata, Logics, and Infinite Games. LNCS, vol. 2500, pp. 3–21. Springer, Heidelberg (2002) CrossRef
15.
Halpern, J.Y., van der Meyden, R., Vardi, M.Y.: Complete axiomatizations for reasoning about knowledge and time. SIAM J. Comput. 33(3), 674–703 (2004)MathSciNetCrossRefMATH
16.
Halpern, J.Y., Vardi, M.Y.: The complexity of reasoning about knowledge and time. 1. Lower bounds. J. Comp. Sys. Sci. 38(1), 195–237 (1989)MathSciNetCrossRefMATH
17.
Janin, D., Walukiewicz, I.: On the expressive completeness of the propositional mu-calculus with respect to monadic second order logic. In: Sassone, V., Montanari, U. (eds.) CONCUR 1996. LNCS, vol. 1119. Springer, Heidelberg (1996)
18.
Matz, O., Schweikardt, N., Thomas, W.: The monadic quantifier alternation hierarchy over grids and graphs. Inf. Comput. 179(2), 356–383 (2002)MathSciNetCrossRefMATH
19.
Maubert, B., Pinchinat, S.: Jumping automata for uniform strategies. In: Proceedings of FSTTCS 2013, pp. 287–298 (2013)
20.
Park, D.: Concurrency and automata on infinite sequences. In: Deussen, P. (ed.) Proceedings of 5th GI Conference on Theoretical Computer Science. Lecture Notes in Computer Science, vol. 104, pp. 167–183. Springer, Heidelberg (1981)CrossRef
21.
Pnueli, A., Rosner, R.: On the synthesis of a reactive module. In: POPL 1989, pp. 179–190. ACM Press (1989)
22.
Puchala, B.: Asynchronous omega-regular games with partial information. In: Hliněný, P., Kučera, A. (eds.) MFCS 2010. LNCS, vol. 6281, pp. 592–603. Springer, Heidelberg (2010) CrossRef
23.
24.
25.
Thomas, W.: Infinite trees and automaton-definable relations over omega-words. Theor. Comput. Sci. 103(1), 143–159 (1992)CrossRefMATH
26.
Thomas, W.: Languages, automata, and logic. In: Rozenberg, G., Salomaa, A. (eds.) Handbook of Formal Languages: Volume 3 Beyond Words, pp. 389–455. Springer, Heidelberg (1997)CrossRef
27.
van der Meyden, R., Shilov, N.V.: Model checking knowledge and time in systems with perfect recall. In: Pandu Rangan, C., Raman, V., Sarukkai, S. (eds.) FST TCS 1999. LNCS, vol. 1738, pp. 432–445. Springer, Heidelberg (1999) CrossRef
28.
Vardi, M.Y.: Reasoning about the past with two-way automata. In: Larsen, K.G., Skyum, S., Winskel, G. (eds.) ICALP 1998. LNCS, vol. 1443, pp. 628–641. Springer, Heidelberg (1998) CrossRef
29.
Metadata
Title
Relating Paths in Transition Systems: The Fall of the Modal Mu-Calculus
Authors
Cătălin Dima
Bastien Maubert
Sophie Pinchinat
Copyright Year
2015
Publisher
Springer Berlin Heidelberg
Book
Mathematical Foundations of Computer Science 2015

Print ISBN: 978-3-662-48056-4

Electronic ISBN: 978-3-662-48057-1

Copyright Year: 2015

DOI
https://doi.org/10.1007/978-3-662-48057-1_14

Premium Partner

    Image Credits