Abstract (click to open/close)

Behavioral verification of technical systems involving both discrete and continuous components is a common and demanding task. The behavior of such systems can often be characterized using stochastic hybrid automata, leading to verification problems which can be formalized and solved using stochastic logic calculi such as stochastic satisfiability modulo theory (SSMT). While algorithms for discharging proof obligations in SSMT form exist, their applicability is limited due to the computational complexity, which often increases exponentially with the number of quantified variables. Recently, statistical model checking has been successfully applied to stochastic hybrid systems, thereby increasing the size of the system for which verification problems is tractable. However, being based on randomized simulation, these methods usually cannot handle non-determinism. In previous work, we have deviated from the usual approach of simulating the model and rather proposed a statistical method for SSMT solving which, being based on statistical AI planning algorithms, can also treat non-determinism over a finite domain. Here, we extend this previous work to the case of continuous domains. In particular, using ideas from noisy optimization, we adaptively build up a decision tree recording the findings and guiding further exploration, thereby favoring the currently most promising sub-domain. The non-determinism is resolved by translating the satisfaction problem into an optimization problem, thereby computing both optimistic and pessimistic bounds on the probability of satisfaction. At each stage of the evaluation process, we show how to obtain confidence statements about the probability of satisfaction for the overall SSMT formula, including reliable estimates on the optimal resolution of any non-deterministic choice involved.

Keywords: Statistical model checking; Stochastic hybrid systems; Non-determinism; SSMT
Subproject(s): H1/2

Abstract (click to open/close)

Fault tolerance measures of distributed systems can be calculated precisely by state space analysis of the Markov chain corresponding to the product of the system components. The power of such an approach is inherently confined by the state space explosion, i.e. the exponential growth of the Markov chain in the size of the underlying system. We propose a decompositional method to alleviate this limitation. Lumping is a well-known reduction technique facilitating computation of the relevant measures on the quotient of the Markov chain under lumping equivalence. In order to avoid computation of lumping equivalences on intractably large Markov chains, we propose a system decomposition supporting local lumping on the considerably smaller Markov chains of the subsystems. Recomposing the lumped Markov chains of the subsystems constructs a lumped transition model of the whole system, thus avoiding the construction of the full product chain. An example demonstrates how the limiting window availability (i.e. a particular fault tolerance measure) can be computed for a self-stabilizing system exploiting lumping and decomposition.

Keywords: Fault tolerance, Self stabilization, Probabilistic model checking, Probabilistic bisimilarity, Markov chains, Limiting window availability
Subproject(s): H4

Abstract (click to open/close)

Aiming at automatic verification and analysis techniques for hybrid discrete-continuous systems, we present a novel combination of enclosure methods for ordinary differential equations (ODEs) with the iSAT solver for large Boolean combinations of arithmetic constraints. Improving on our previous work, the contribution of this paper lies in combining iSAT with VNODE-LP, as a state-of-the-art interval solver for ODEs, and with bracketing systems, which exploit monotonicity properties allowing to find enclosures for problems that VNODE-LP alone cannot enclose tightly. We apply the combined iSAT-ODE solver to the analysis of a variety of non-linear hybrid systems by solving predicative encodings of reachability properties and of an inductive stability argument, and evaluate the impact of the different enclosure methods, decision heuristics and their combination. Our experiments include classic benchmarks from the literature, as well as a newly-designed conveyor belt system that combines hybrid behavior of parallel components, a slip-stick friction model with non-linear dynamics and flow invariants and several dimensions of parameterization. In the paper, we also present and evaluate an extension of VNODE-LP tailored to its use as a deduction mechanism within iSAT-ODE, to allow fast re-evaluations of enclosures over arbitrary subranges of the analyzed time span.

Keywords: Analysis of hybrid discrete-continuous systems; Satisfiability modulo theories; Enclosure methods for ODEs; Bracketing systems
Subproject(s): H1/2

Abstract (click to open/close)

The stochastic Boolean satisfiability (SSAT) problem has been introduced by Papadimitriou in 1985 when adding a probabilistic model of uncertainty to propositional satisfiability through randomized quantification. SSAT has many applications, among them probabilistic bounded model checking (PBMC) of symbolically represented Markov decision processes. This article identifies a notion of emph Craig interpolant for the SSAT framework and develops an algorithm for computing such interpolants based on a resolution calculus for SSAT. As a potential application area of this novel concept of Craig interpolation, we address the symbolic analysis of probabilistic systems. We first investigate the use of interpolation in probabilistic state reachability analysis, turning the falsification procedure employing PBMC into a verification technique for probabilistic safety properties. We furthermore propose an interpolation-based approach to probabilistic region stability, being able to verify that the probability of stabilizing within some region is sufficiently large.

Subproject(s): H1/2,H4

Abstract (click to open/close)

In previous publications, the authors have introduced the notion of stochastic satisfiability modulo theories (SSMT) and the corresponding SiSAT solving algorithm, which provide a symbolic method for the reachability analysis of probabilistic hybrid systems. SSMT extends satisfiability modulo theories (SMT) with randomized (or stochastic), existential, and universal quantification, as known from stochastic propositional satisfiability. In this paper, we extend the SSMT-based procedures to the symbolic analysis of concurrent probabilistic hybrid systems. After formally introducing the computational model, we provide a mechanized translation scheme to encode probabilistic bounded reachability problems of concurrent probabilistic hybrid automata as linearly sized SSMT formulae, which in turn can be solved by the SiSAT tool. We furthermore propose an algorithmic enhancement which tailors SiSAT to probabilistic bounded reachability problems by caching and reusing solutions obtained on bounded reachability problems of smaller depth. An essential part of this article is devoted to a case study from the networked automation systems domain. We explain in detail the formal model in terms of concurrent probabilistic automata, its encoding into the SiSAT modeling language, and finally the automated quantitative analysis.

Keywords: Concurrent probabilistic hybrid systems, probabilistic logic, constraint satisfaction problems, problem solvers, automatic verification
Subproject(s): H1/2,H4

Abstract (click to open/close)

In this article, we recall different approaches to the constraint-based, symbolic analysis of hybrid discrete-continuous systems and combine them to a technology able to address hybrid systems exhibiting both non-deterministic and probabilistic behavior akin to infinite-state Markov decision processes. To enable mechanized analysis of such systems, we extend the reasoning power of arithmetic satisfiability-modulo-theories (SMT) solving by, first, reasoning over ordinary differential equations (ODEs) and, second, a comprehensive treatment of randomized (also known as stochastic) quantification over discrete variables as well as existential quantification over both discrete and continuous variables within the mixed Boolean-arithmetic constraint system. This provides the technological basis for a constraint-based analysis of dense-time probabilistic hybrid automata, extending previous results addressing discrete-time automata (1). Generalizing SMT-based bounded model-checking of hybrid automata (2; 3), stochastic SMT including ODEs permits the direct analysis of probabilistic bounded reachability problems of dense-time probabilistic hybrid automata without resorting to approximation by intermediate finite-state abstractions.

Keywords: Probabilistic hybrid automata, bounded model checking, arithmetic constraint solving, stochastic satisfiability
Subproject(s): H1/2,H4

Abstract (click to open/close)

Bounded model checking (BMC) is an incremental refutation technique to search for counterexamples of increasing length. The existence of a counterexample of a fixed length is expressed by a first-order logic formula that is checked for satisfiability using a suitable solver. We apply communicating parallel solvers to check satisfiability of the BMC formulae. In contrast to other parallel solving techniques, our method does not parallelize the satisfiability check of a single formula, but the parallel solvers work on formulae for different counterexample lengths. We adapt the method of constraint sharing and replication of Shtrichman, originally developed for sequential BMC, to the parallel setting. Since the learning mechanism is now parallelized, it is not obvious whether there is a benefit from the concepts of Shtrichman in the parallel setting. We demonstrate on a number of benchmarks that adequate communication between the parallel solvers yields the desired results.

Keywords: parallel programs, bounded model checking, SAT solving, linear programming, hybrid systems
Subproject(s): H1/2

Abstract (click to open/close)

Duration Calculus (abbreviated to DC) is an interval-based, metric-time temporal logic designed for reasoning about embedded real-time systems at a high level of abstraction. But the complexity of model checking any decidable fragment featuring both negation and chop, DC’s only modality, is non-elementary and thus impractical. Even worse, when such decidable fragments are generalized just slightly to cover more interesting durational constraints the resulting fragments become undecidable. We here investigate a similar approximation as frequently employed in model checking situation- or point-based temporal logics, where linear-time problems are safely approximated by branching-time counterparts amenable to more efficient model-checking algorithms. Mimicking the role that a situation has in (A)CTL as the origin of a set of linear traces, we define a branching-time counterpart to interval-based temporal logics building on situation pairs spanning sets of intervals. While this branching-time interval semantics yields the desired reduction in complexity of the model-checking problem, from undecidable to linear in the size of the formula and cubic in the size of the model, the approximation is too coarse to be practical. We therefore refine the semantics by an occurrence count for crucial states (e.g., cuts of loops) in the model, arriving at a 4-fold exponential model-checking problem sufficiently accurately approximating the original one. Furthermore, when chop occurs in negative polarity only in DC formulas, we have a doubly exponential model-checking algorithm.

Subproject(s): R1

Abstract (click to open/close)

The Transregional Collaborative Research Center AVACS integrates the three sites Freiburg, Oldenburg, and Saarbr�cken and addresses the challenge of pushing the borderline for automatic verification and analysis of complex systems. A particular focus of the project is on models of complex transportation systems and their safety requirements. AVACS is organized in ten subprojects, each teaming researchers from all sites, and is funded by the German Science Foundation since January 1, 2004. This articles surveys scope, organization and research directions of AVACS, including pointers to key publications.

Subproject(s): R1,R2,R3,H1,H2,H3,H4,S1,S2,S3

Abstract (click to open/close)

In this paper we present HySAT, a new bounded model checker for linear hybrid systems, incorporating a tight integration of a DPLL-based pseudo-Boolean SAT solver and a linear programming routine as core engine. In contrast to related tools like MathSAT, ICS, or CVC, our tool exploits all of the various optimizations that arise naturally in the bounded model checking context, e.g. isomorphic replication of learned conflict clauses or tailored decision strategies, and extends them to the hybrid domain. We demonstrate that those optimizations are crucial to the performance of the tool.

Keywords: verification, bounded model checking, hybrid systems, infinite-state systems, decision procedures, satisfiability
Subproject(s): H2

Abstract (click to open/close)

In order to facilitate automated reasoning about large Boolean combinations of non-linear arithmetic constraints involving transcendental functions, we provide a tight integration of recent SAT solving techniques with interval-based arithmetic constraint solving. Our approach deviates substantially from lazy theorem proving approaches in that it directly controls arithmetic constraint propagation from the SAT solver rather than delegating arithmetic decisions to a subordinate solver. Through this tight integration, all the algorithmic enhancements that were instrumental to the enormous performance gains recently achieved in propositional SAT solving do smoothly carry over to the rich domain of non-linear arithmetic constraints. As a consequence, our approach is able to handle large constraint systems with extremely complex Boolean structure, involving Boolean combinations of multiple thousand arithmetic constraints over some thousands of variables.

Subproject(s): H1,H2

Subproject(s): H1