Change search
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • 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
Logics and Algorithms for Verification of Concurrent Systems
Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Division of Computing Science. Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computing Science.
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: urn:nbn:se:uu:diva-179847ISBN: 978-91-554-8447-7 (print)OAI: oai:DiVA.org:uu-179847DiVA: diva2:546861
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
List of papers
1. Parallel model checking for LTL, CTL* and Lmu2
Open this publication in new window or tab >>Parallel model checking for LTL, CTL* and Lmu2
2003 (English)In: PDMC 2003: 2nd International Workshop on Parallel and Distributed Model Checking, 2003, 4-16 p.Conference paper, Published paper (Refereed)
National Category
Computer Engineering Computer Science
Identifiers
urn:nbn:se:uu:diva-48668 (URN)
Available from: 2006-12-15 Created: 2006-12-15 Last updated: 2013-01-22
2. The Complexity of Model Checking Higher Order Fixpoint Logic
Open this publication in new window or tab >>The Complexity of Model Checking Higher Order Fixpoint Logic
2005 (English)In: Mathematical Foundations of Computer Science 2005: 30th International Symposium, MFCS 2005, Gdansk, Poland, August 29–September 2, 2005. Proceedings, 2005Conference paper, Published paper (Refereed)
Identifiers
urn:nbn:se:uu:diva-80124 (URN)doi:10.1007/11549345_55 (DOI)3-540-28702-7 (ISBN)
Available from: 2006-04-25 Created: 2006-04-25 Last updated: 2013-01-22
3. Propositional dynamic logic of context-free programs and fixpoint logic with chop
Open this publication in new window or tab >>Propositional dynamic logic of context-free programs and fixpoint logic with chop
2006 (English)In: Information Processing Letters, ISSN 0020-0190, E-ISSN 1872-6119, Vol. 100, no 2, 72-75 p.Article in journal (Refereed) Published
Abstract [en]

This paper compares propositional dynamic logic of non-regular programs and fixpoint logic with chop. It identifies a fragment of the latter which is equi-expressive to the former. This relationship transfers several decidability and complexity results between the two logics.

Keyword
program specification, formal languages, concurrency
National Category
Computer Science
Identifiers
urn:nbn:se:uu:diva-107987 (URN)10.1016/j.ipl.2006.04.019 (DOI)000240296300007 ()
Available from: 2009-09-02 Created: 2009-09-02 Last updated: 2017-12-13Bibliographically approved
4. The Complexity of Model Checking Higher-order Fixpoint Logic
Open this publication in new window or tab >>The Complexity of Model Checking Higher-order Fixpoint Logic
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.

Keyword
mu-calculis, lambda-calculus, model checking, complexity
National Category
Computer and Information Science
Identifiers
urn:nbn:se:uu:diva-107983 (URN)10.2168/lmcs-3(2:7)2007 (DOI)000262497200006 ()
Available from: 2009-09-02 Created: 2009-09-02 Last updated: 2017-12-13Bibliographically approved
5. Accelerated Approximation for Stochastic Reachability Games: Extended version of paper New algorithms for solving simple stochastic games
Open this publication in new window or tab >>Accelerated Approximation for Stochastic Reachability Games: Extended version of paper New algorithms for solving simple stochastic games
2010 (English)Other (Other academic)
Abstract [en]

In this paper new algorithms for finding optimal values and strategies inturn-based stochastic games with reachability objectives are presented,whose special case are the simple stochastic games considered elsewhere [4,11]. The general idea of these algorithms is to accelerate the successive approximation scheme for solving stochastic games [13] in which node values are updated in each iteration so that they converge to the optimal values of the game. This scheme is extended with a pair of positional strategies which are updated to remain greedy with respect to the current approximation. This way optimal strategies can be discovered before the current values get close to the optimal ones. The approximation process is accelerated, by predicting an approximate result of several updates of the current valuation and jumping directly to the predicted values.

New algorithms are based on three different acceleration techniques: iterative squaring, linear extrapolation, and linear programming; with different difficulty of performing single iteration and different acceleration level achieved by each of them. For each of these algorithms the complexity of a single iteration is polynomial. It is shown that accelerated algorithms will never perform worse than the basic, non-accelerated one and exponential upper bounds on the number of iterations required to solve a game in the worst case is given. It is also proven that new algorithms increase the frequency with which the greedy strategies are updated. The more often strategies are updated, the higher chances that the algorithm will terminate early. It is proven that the algorithm based on linear programming updates the greedy strategies in every iteration, which makes it similar to the strategy improvement method, where also a new strategy is found in each iteration and this also at the cost of solving linear constraint problems

Paper is concluded with presentation of results of experiments in which new algorithms were run on a sample of randomly generated games. It could be observed that the proposed acceleration techniques reduce the number of iterations of the basic algorithm by an order of magnitude and that they substantially increase frequency with which the greedy strategies are updated. The algorithms based on linear programming and linear extrapolation displayed similar efficiency as the ones based on strategy improvement. This makes the algorithm based on linear extrapolation especially attractive because it uses much simpler computations than linear constraint solving.

Keyword
simple stochastic games, successive approximation, strategy improvement, complexity
National Category
Computer Science
Research subject
Computer Science
Identifiers
urn:nbn:se:uu:diva-179845 (URN)
Note

The original paper was published in Proceedings of the Workshop on Games in Design and Verification (GDV 2004), volume 119 of Electronic Notes in Theoretical Computer Science, pages 51–65. Elsevier. http://dx.doi.org/10.1016/j.entcs.2004.07.008

Available from: 2012-08-24 Created: 2012-08-24 Last updated: 2013-01-22Bibliographically approved

Open Access in DiVA

fulltext(1081 kB)353 downloads
File information
File name FULLTEXT01.pdfFile size 1081 kBChecksum SHA-512
d2e2995f810a729494f6825e4c2bb1fbf3005cc6c6b8947f0d329cbadf86b8aaa0df138b566cd62a3e378555cc0e54f98a9de7ba2080d5cd25f08a1724e0010b
Type fulltextMimetype application/pdf
Buy this publication >>

Search in DiVA

By author/editor
Somla, Rafał
By organisation
Division of Computing ScienceComputing Science
Computer Science

Search outside of DiVA

GoogleGoogle Scholar
Total: 353 downloads
The number of downloads is the sum of all downloads of full texts. It may include eg previous versions that are now no longer available

isbn
urn-nbn

Altmetric score

isbn
urn-nbn
Total: 634 hits
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • 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