Ergebnisse der Suche:
- [Ellen et al.,
2014]
- Christian Ellen, Sebastian Gerwinn, and Martin
Fränzle.
Statistical
model checking for stochastic hybrid systems involving nondeterminism over
continuous domains.
International Journal on Software Tools for Technology Transfer,
pages 1-20, 2014.
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
|
|  Bibtex
|  PDF restricted |
- [Müllner et al.,
2013]
- Nils Müllner, Oliver Theel, and Martin Fränzle.
Combining decomposition and reduction for state space analysis of a
self-stabilizing system.
Journal of Computer and System Sciences (JCSS), 79(7):1113-1125,
2013.
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
|
|  Bibtex
|  PDF restricted |
- [Eggers et al.,
2012a]
- Andreas Eggers, Nacim Ramdani, Nedialko S. Nedialkov,
and Martin Fränzle.
Improving
the SAT modulo ODE approach to hybrid systems analysis by combining
different enclosure methods.
Software & Systems Modeling, 2012.
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
|
|  Bibtex
|  PDF restricted |
- [Teige and Fränzle,
2012]
- Tino Teige and Martin Fränzle.
Generalized Craig interpolation for stochastic Boolean satisfiability
problems with applications to probabilistic state reachability and region
stability.
Logical Methods in Computer Science, 8(2):1-32, 2012.
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
|
|  Bibtex
|  PDF open |
- [Teige et al.,
2011]
- Tino Teige, Andreas Eggers, and Martin Fränzle.
Constraint-based analysis of concurrent probabilistic hybrid systems: An
application to networked automation systems.
Nonlinear Analysis: Hybrid Systems, 5(2):343-366, 2011.
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
|
|  Bibtex
|  PDF restricted |
- [Fränzle et al.,
2010a]
- Martin Fränzle, Tino Teige, and Andreas Eggers.
Engineering constraint solvers for automatic analysis of probabilistic
hybrid automata.
Journal of Logic and Algebraic Programming, 79(7):436-466, 2010.
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
|
|  Bibtex
|  PDF restricted |
- [Ábrahám et al.,
2009]
- Erika Ábrahám, Tobias Schubert, Bernd Becker,
Martin Fränzle, and Christian Herde.
Parallel SAT
solving in bounded model checking.
Journal of Logic and Computation, pages 301-315, 2009.
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
|
|  Bibtex
|  PDF restricted |
- [Fränzle and Hansen, 2009]
- Martin Fränzle
and Michael R. Hansen.
Efficient model checking for duration calculus.
International Journal of Software and Informatics,
3(2-3):171-196, 2009.
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
|
|  Bibtex
|  PDF restricted |
- [Becker et al.,
2007a]
- Bernd Becker, Werner Damm, Martin Fränzle,
Ernst-Rüdiger Olderog, Andreas Podelski, and Reinhard Wilhelm.
SFB/TR 14 AVACS -- automatic verification and analysis of complex
systems.
it -- Information Technology, 49(2):118-126, 2007.
http://it-Information-Technology.de, DOI 10.1524/itit.2007.49.2.118.
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
|
|  Bibtex
|  PDF open |
- [Fränzle and Herde,
2007]
- Martin Fränzle and Christian Herde.
HySAT: An
efficient proof engine for bounded model checking of hybrid systems.
Formal Methods in System Design, 30:179-198, 2007.
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
|
|  Bibtex
|  PostScript restricted |
 PDF restricted |
- [Fränzle et al.,
2007a]
- Martin Fränzle, Christian Herde, Stefan Ratschan,
Tobias Schubert, and Tino Teige.
Efficient solving of large non-linear arithmetic constraint systems with
complex boolean structure.
Journal on Satisfiability, Boolean Modeling and Computation -- Special
Issue on SAT/CP Integration, 1:209-236, 2007.
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
|
|  Bibtex
|  PDF restricted |
- [Fränzle,
2004]
- Martin Fränzle.
Model-checking dense-time duration calculus.
Formal Aspects of Computing Science, 16(2):121-139, 2004.
Subproject(s): H1
|
|  Bibtex
|  PDF restricted |
|