Published: 23rd February 2014 DOI: 10.4204/EPTCS.140 ISSN: 2075-2180 |
Preface | |
Lattice structures for bisimilar Probabilistic Automata Johann Schuster and Markus Siegle | 1 |
A Finite Exact Representation of Register Automata Configurations Yu-Fang Chen, Bow-Yaw Wang and Di-De Yen | 16 |
Zenoness for Timed Pushdown Automata Parosh Aziz Abdulla, Mohamed Faouzi Atig and Jari Stenman | 35 |
Invited Tutorial:
Algorithmic Verification of Continuous and Hybrid Systems Oded Maler | 48 |
Invited Tutorial:
Synthesis of Parametric Programs using Genetic Programming and Model Checking Gal Katz and Doron Peled | 70 |
Invited Tutorial:
Automated Analysis of Probabilistic Infinite-state Systems Dominik Wojtczak | 85 |
Presentation:
Decidability Results for Well-structured Graph Transformation Systems Barbara König and Jan Stückrath | 87 |
This volume contains the proceedings of the 15th International Workshop on Verification of Infinite-State Systems (INFINITY'13). The workshop was held in Hanoi, Vietnam on October 14, 2013, as a satellite event to the 11th International Symposium on Automated Technology for Verification and Analysis (ATVA'13).
The aim of the INFINITY workshop is to provide a forum for researchers interested in the development of formal methods and algorithmic techniques for the analysis of systems with infinitely many states, and their application in automated verification of complex software and hardware systems.
Topics of interest include (but are not limited to):This volume contains seven contributions: three regular papers, one presentation, and three invited tutorials. Each regular paper was reviewed by four different reviewers. The papers were refereed by the program committee and by external referee Cong Quy Trinh, whose help is gratefully acknowledged. Each invited tutorial was reviewed by the editors before acceptance. Moreover, the program committee of INFINITY 2013 has selected the following presentation:
The program of INFINITY 2013 was further enriched by four invited talks given by
The INFINITY'13 workshop was attended by 21 participants. It has been organized as a satellite event to ATVA'13. We thank the authors for their contributions, the programme committee members for reviewing and selecting the papers and the invited talks, and the ATVA organizing committee Mizuhito Ogawa and Truong Anh Hoang for their support.
The final proceedings will appear in the Electronic Proceedings in Theoretical Computer Science (EPTCS) series. We thank Rob Van Glabbeek (Editor-in-Chief) and the board of the EPTCS for making this possible.
Bordeaux and Brno, December 2013 | Lorenzo Clemente and Lukáš Holík |
Lorenzo Clemente | University of Bordeaux | France |
Lukáš Holík | Brno University of Technology | Czech Republic |
Parosh Abdulla | Uppsala University | Sweden |
Mohamed F. Atig | Uppsala University | Sweden |
Giorgio Delzanno | University of Genova | Italy |
Peter Habermehl | LIAFA, Univ. Denis Diderot---Paris 7, CNRS | France |
Anthony W. Lin | University of Oxford | United Kingdom |
Richard Mayr | University of Edinburgh | United Kingdom |
Jean-François Raskin | Université Libre de Bruxelles | Belgium |
Ahmed Rezine | Linköping University | Sweden |
Jiří Srba | Aalborg University | Denmark |
Grégoire Sutre | University of Bordeaux I | France |
Tomáš Vojnar | Brno University of Technology | Czech Republic |
Bow-Yaw Wang | Academia Sinica | Taiwan |
In this talk we survey the state of the art in the automated analysis of several classes of finitely-presentable infinite-state probabilistic models which combine probabilistic, recursive and in many cases also controlled or more general game behaviour. Unreliability is inherent to almost all physical systems, e.g. telecommunication networks, distributed systems, railway connections. Software systems, designed with robustness and efficiency in mind, often make explicit use of randomness, thus exhibiting probabilistic behaviour. Also, even if a system or a program behaves deterministically, the environment were it operates is in many cases either unknown or very complex. In such situations the best we can hope for is to statistically quantify the behaviour of the environment and analyse the performance of our model in such a probabilistic setting. It is common to model purely probabilistic systems as finite-state Markov Chains or as Markov Decision Processes if the system is both probabilistic and controlled. However, to faithfully represent the behaviour of many naturally occurring systems one really needs to represent them as infinite-state Markov Chains or Markov Decision Processes. This is because finite-state probabilistic models differ significantly from infinite-state ones, e.g. in finite-state systems no null recurrent states can occur, i.e. states that are revisited with probability 1, but with infinite expected time before this happens.
The finitely-presentable infinite-state probabilistic models studied in the literature include Multi-Type Branching Processes (see, e.g. [12, 10]), Stochastic Context-Free Grammars (see, e.g. [13, 1]), Quasi-Death-Birth processes (see, e.g. [14, 15]), "random walks with back-buttons" [9], Recursive Markov Chains [8] and probabilistic Pushdown Systems [4]. These models found applications in domains as diverse as population dynamics, nuclear chain reactions, natural language processing, biological sequence analysis, red blood cells formation, queueing theory, modelling web surfing and finally model checking of probabilistic procedural programs. The relationship of the expressive power of these particular models have been extensively studied, e.g. in [7] where a tight connection was established to the the models used in the queueing theory, but the first natural model that subsumes all of the mentioned models was defined in [11].
The fundamental quantitative analysis of these models can be done by constructing a specific system of monotone polynomial equations and finding its least nonnegative fixed point. In order to find this fixed point efficiently we can use, e.g. numerical approximation methods such as Jacobi iteration, Gauss-Seidel iteration or a decomposed variant of the Newton's method as described in [8]. A detailed analysis of the theoretical performance of the Newton's method when applied in this setting was done in [3, 5]. Here we look instead on how well it performs in practice and describe a tool called PReMo [17] (Probabilistic Recursive Models analyser) which implements highly optimised versions of these approximation algorithms in Java. Using simple tailored-made input languages PReMo is able to accept Recursive Markov Chains and Stochastic Context-Free grammars as an input, while the other models can be easily translated into these ones. PReMo is able to perform all kind of analyses such as computing the termination probability (as described in [8]), the expected termination time (as in [6]) or the standard deviation of that time (as in [2]) among others. PReMo's performance was tested on Stochastic Context-Free Grammars derived from the Penn Treebank corpora in [17], on queuing models in [7] and on many other examples in [16].
The general domain of finitely-presented infinite-state probabilistic models is a rich and fascinating field of study that is getting more and more attention. Many important questions regarding the computational complexity of their analysis were already addressed and there is a tool that is able to analyse them efficiently. However, many theoretical questions still remain open, and there is still a potential of improving the performance of PReMo, the range of quantitative analyses and input models it supports.
Well-structured transition systems [1, 4] are one of the main sources for decidability results for infinite-state systems. Well-structured transition systems equip a state space with a partial order, which must be a well-quasi-order and a simulation relation for the transition relation. If a system can be seen as a well-structured transition system, one can decide the coverability problem, i.e., the problem of verifying whether, from a given start state, one can reach a state that covers a final state, i.e., is larger than the final state with respect to the chosen order by a generic backward reachability algorithm. Often, these given final states, and all larger states, are considered to be error states and one can hence check whether an error state is reachable.
This can also be done for graph transformation systems [9], a natural specification language for concurrent, distributed systems with a variable topology. In those systems states are represented by (hyper-)graphs and state changes by (local) transformation rules, consisting of a left-hand and a right-hand side.
In [5] we showed how certain lossy graph transformation systems with edge contraction rules can be viewed as well-structured transition systems with respect to the graph minor ordering [7, 8] and applied the theory to verify a leader election protocol. In later work [2] we treated another case study and analysed a termination detection protocol. The technique works for arbitrary graphs, since the minor ordering is a well-quasi-order on all graphs, but requires certain restrictions on the rule sets to obtain well-structuredness, namely the existence of edge contraction rules.
Here we will extend the approach of [5] to a general framework [6], which can handle arbitrary orders and state sufficient conditions for the backward search to be correct. We consider the subgraph ordering and the induced subgraph ordering as alternatives to the minor ordering.
Opposed to the minor ordering, the subgraph ordering is not a well-quasi-order on the set of all graphs, but only on those graphs where the length of paths is bounded. This results in a trade-off: while the stricter order allows us to consider all possible sets of graph transformation rules (we show that these systems are all well-structured w.r.t. the subgraph ordering), we have to make sure to consider a system where only graphs satisfying this restriction are reachable. Furthermore, we gain precision in the specification of final graphs, since we can represent them via subgraphs instead of minors. The induced subgraph ordering, apart from being more precise in the specification of error graphs, in addition allows restricted negative application conditions on the rules. It turns out that the results and proofs of [5] can be transferred to this new setting.
Apart from the orders mentioned above, there are various other well-quasi-orders on graphs that could be used [3], leading to different classes of systems and different notions of coverability. Our framework can handle such partial orders if they can be represented by (partial) graph morphisms and satisfy some preservation criteria with respect to pushouts of graphs.