uu.seUppsala University Publications
Change search
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf
The Complexity of Model Checking Higher-order Fixpoint Logic
Department of Computer Science, University of Munich.
Department of Computer Science, University of Munich.
Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computing Science.
2007 (English)In: Logical Methods in Computer Science, ISSN 1860-5974, E-ISSN 1860-5974, Vol. 3, no 2:7, 1-33 p.Article in journal (Refereed) Published
Abstract [en]

Higher-Order Fixpoint Logic (HFL) is a hybrid of the simply typed λ-calculus and the modal μ-calculus. This makes it a highly expressive temporal logic that is capable of expressing various interesting correctness properties of programs that are not expressible in the modal μ-calculus. This paper provides complexity results for its model checking problem. In particular we consider those fragments of HFL built by using only types of bounded order k and arity m. We establish k-fold exponential time completeness for model checking each such fragment. For the upper bound we use fixpoint elimination to obtain reachability games that are singly-exponential in the size of the formula and k-fold exponential in the size of the underlying transition system. These games can be solved in deterministic linear time. As a simple consequence, we obtain an exponential time upper bound on the expression complexity of each such fragment. The lower bound is established by a reduction from the word problem for alternating (k-1)-fold exponential space bounded Turing Machines. Since there are fixed machines of that type whose word problems are already hard with respect to k-fold exponential time, we obtain, as a corollary, k-fold exponential time completeness for the data complexity of our fragments of HFL, provided m exceeds 3. This also yields a hierarchy result in expressive power.

Place, publisher, year, edition, pages
2007. Vol. 3, no 2:7, 1-33 p.
Keyword [en]
mu-calculis, lambda-calculus, model checking, complexity
National Category
Computer and Information Science
Identifiers
URN: urn:nbn:se:uu:diva-107983DOI: 10.2168/lmcs-3(2:7)2007ISI: 000262497200006OAI: oai:DiVA.org:uu-107983DiVA: diva2:233843
Available from: 2009-09-02 Created: 2009-09-02 Last updated: 2017-12-13Bibliographically approved
In thesis
1. Logics and Algorithms for Verification of Concurrent Systems
Open this publication in new window or tab >>Logics and Algorithms for Verification of Concurrent Systems
2012 (English)Doctoral thesis, comprehensive summary (Other academic)
Abstract [en]

In this thesis we investigate how the known framework of automatic formal verification by model checking can be extended in different directions. One extension is to go beyond the common limitation of the existing specification formalisms, that they can describe only regular properties of components. This can be achieved using logics capable of expressing non-regular properties, such as the Propositional Dynamic Logic of Context-free Programs (PDLCF), Fixpoint Logic with Chop (FLC) or the Higher-order Fixpoint Logic (HFL). Our main result in this area is proving that the problem of model checking HFL formulas of order bounded by k is k-EXPTIME complete. In the proofs we demonstrate two model checking algorithms for that logic. We also show that PDLCF is equivalent to a proper fragment of FLC.

The standard model checking algorithms, which are run on a single computer, are severely limited by the amount of available computing resources. A way to overcome this limitation is to develop distributed algorithms, which can be run on a cluster of computers and use their joint resources. In this thesis we show how a distributed model checking algorithm for the alternation-free fragment of the modal μ-calculus can be extended to handle formulas with one level of alternation. This is an important extension, since Lμ formulas with one level of alternation can express the same properties as logics LTL and CTL commonly used in formal verification.

Finally, we investigate stochastic games which can be used to model additional aspects of components, such as their interaction with environment and their quantitative properties. We describe new algorithms for finding optimal values and strategies in turn-based stochastic games with reachability winning conditions. We prove their correctness and report on experiments where we compare them against each other and against other known algorithms, such as value iteration and strategy improvement.

Place, publisher, year, edition, pages
Uppsala: Acta Universitatis Upsaliensis, 2012. 48 p.
Series
Digital Comprehensive Summaries of Uppsala Dissertations from the Faculty of Science and Technology, ISSN 1651-6214 ; 964
National Category
Computer Science
Research subject
Computer Science
Identifiers
urn:nbn:se:uu:diva-179847 (URN)978-91-554-8447-7 (ISBN)
Public defence
2012-10-01, Room 2446, Polacksbacken, Lägerhyddsvägen 2, Uppsala, 13:15 (English)
Opponent
Supervisors
Available from: 2012-09-11 Created: 2012-08-24 Last updated: 2014-07-21Bibliographically approved

Open Access in DiVA

No full text

Other links

Publisher's full text
By organisation
Computing Science
In the same journal
Logical Methods in Computer Science
Computer and Information Science

Search outside of DiVA

GoogleGoogle Scholar

doi
urn-nbn

Altmetric score

doi
urn-nbn
Total: 522 hits
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf