Skip to main content
Fachgebiete
Automobil + Motoren Bauwesen + Immobilien Business IT + Informatik Elektrotechnik + Elektronik Energie + Nachhaltigkeit Finance + Banking Management + Führung Marketing + Vertrieb Maschinenbau + Werkstoffe Versicherung + Risiko
DE
EN
Themenseiten
Organisationspsychologie Projektmanagement Marketing Smart Manufacturing
Bücher
Zeitschriften
Weitere Formate
Podcasts Webinare Technik Webinare Wirtschaft Kongresse Veranstaltungskalender Awards
Jetzt Einzelzugang starten
Zugang für Unternehmen
Referenzkunden
MTZ-Fachkongress

Antriebe und Energiesysteme von morgen


Austausch von Automobil- und Energiewirtschaft

Am 14./15. Mai geht es in Chemnitz um die Mobilitätswende durch Elektro- und Wasserstofffahrzeuge.
Erweiterte Suche
Anmelden
nach oben
Erschienen in:
The Multiple Dimensions of Mean-Payoff Games Kapitel lesen Erstes Kapitel lesen

2017 | OriginalPaper | Buchkapitel

Space-Efficient Fragments of Higher-Order Fixpoint Logic

verfasst von : Florian Bruse, Martin Lange, Etienne Lozes

Erschienen in: Reachability Problems

Verlag: Springer International Publishing

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config
loading …

Abstract

Higher-Order Fixpoint Logic (HFL) is a modal specification language whose expressive power reaches far beyond that of Monadic Second-Order Logic, achieved through an incorporation of a typed \(\lambda \)-calculus into the modal \(\mu \)-calculus. Its model checking problem on finite transition systems is decidable, albeit of high complexity, namely k-EXPTIME-complete for formulas that use functions of type order at most \(k > 0\). In this paper we present a fragment with a presumably easier model checking problem. We show that so-called tail-recursive formulas of type order k can be model checked in \((k-1)\)-EXPSPACE, and also give matching lower bounds. This yields generic results for the complexity of bisimulation-invariant non-regular properties, as these can typically be defined in HFL.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

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!

Jetzt informieren

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!

Jetzt informieren

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!

Jetzt informieren
Vorheriges Kapitel Adding Dense-Timed Stack to Integer Reset Timed Automata
Nächstes Kapitel Refinement of Trace Abstraction for Real-Time Programs
Literatur
1.
Andersen, H.R.: A polyadic modal \(\mu \)-calculus. Technical Report ID-TR: 1994–195, Dept. of Computer Science, Technical University of Denmark, Copenhagen (1994)
2.
Axelsson, R., Lange, M.: Model checking the first-order fragment of higher-order fixpoint logic. In: Dershowitz, N., Voronkov, A. (eds.) LPAR 2007. LNCS (LNAI), vol. 4790, pp. 62–76. Springer, Heidelberg (2007). doi:10.​1007/​978-3-540-75560-9_​7 CrossRef
3.
Axelsson, R., Lange, M., Somla, R.: The complexity of model checking higher-order fixpoint logic. Logical Meth. Comput. Sci. 3, 1–33 (2007)MathSciNetCrossRefMATH
4.
5.
Harel, D., Pnueli, A., Stavi, J.: Propositional dynamic logic of nonregular programs. J. Comput. Syst. Sci. 26(2), 222–243 (1983)MathSciNetCrossRefMATH
6.
7.
Janin, D., Walukiewicz, I.: On the expressive completeness of the propositional \(\mu \)-calculus with respect to monadic second order logic. In: CONCUR, pp. 263–277 (1996)
8.
Jones, N.D.: The expressive power of higher-order types or, life without CONS. J. Funct. Progm. 11(1), 5–94 (2001)MathSciNetMATH
9.
10.
11.
Lange, M.: Temporal logics beyond regularity. Habilitation thesis, University of Munich, BRICS research report RS-07-13 (2007)
12.
Lange, M., Lozes, E.: Capturing bisimulation-invariant complexity classes with higher-order modal fixpoint logic. In: Diaz, J., Lanese, I., Sangiorgi, D. (eds.) TCS 2014. LNCS, vol. 8705, pp. 90–103. Springer, Heidelberg (2014). doi:10.​1007/​978-3-662-44602-7_​8
13.
Lange, M., Somla, R.: Propositional dynamic logic of context-free programs and fixpoint logic with chop. Inf. Process. Lett. 100(2), 72–75 (2006)MathSciNetCrossRefMATH
14.
Otto, M.: Bisimulation-invariant PTIME and higher-dimensional \(\mu \)-calculus. Theor. Comput. Sci. 224(1–2), 237–265 (1999)MathSciNetCrossRefMATH
15.
Savitch, W.J.: Relationships between nondeterministic and deterministic tape complexities. J. Comput. Syst. Sci. 4, 177–192 (1970)MathSciNetCrossRefMATH
16.
Stearns, R.E., Hartmanis, J., Lewis II, P.M.: Hierarchies of memory limited computations. In: Proceedings of the 6th Annual Symposium on Switching Circuit Theory and Logical Design, pp. 179–190. IEEE (1965)
17.
van Emde Boas, P.: The convenience of tilings. In: Sorbi, A. (ed.) Complexity, Logic, and Recursion Theory, vol. 187 of Lecture Notes in Pure and Applied Mathematics, pp. 331–363. Marcel Dekker Inc (1997)
18.
Metadaten
Titel
Space-Efficient Fragments of Higher-Order Fixpoint Logic
verfasst von
Florian Bruse
Martin Lange
Etienne Lozes
Copyright-Jahr
2017
Buch
Reachability Problems

Print ISBN: 978-3-319-67088-1

Electronic ISBN: 978-3-319-67089-8

Copyright-Jahr: 2017

DOI
https://doi.org/10.1007/978-3-319-67089-8_3

Premium Partner

    Bildnachweise