Ergebnisse der Suche:
 [Scheibler et al.,
2016]
 Karsten Scheibler, Felix Neubauer, Ahmed Mahdi, Martin
Fränzle, Tino Teige, Tom Bienmüller, Detlef Fehrer, and Bernd
Becker.
Extending iSAT3 with ICPcontractors for bitwise integer operations.
AVACS Technical Report No. 116, SFB/TR 14 AVACS, 2016.
ISSN: 18609821, http://www.avacs.org.
Abstract (click to open/close) Up to now SMTsolvers addressing
floatingpoint arithmetic were based on bitblasting. Quite recently, methods
based on interval constraint propagation (ICP) for accurate reasoning over
floatingpoint arithmetic were proposed. One prominent usecase for such
methods is automatic deadcode detection in floatingpoint dominated embedded
C programs. However, C programs usually contain a mix of floatingpoint
arithmetic, integer arithmetic and bitwise integer operations. Thus, adding
ICPbased support for floatingpoint arithmetic is not enough  bitwise
integer operations have to be supported as well. Therefore, this report gives
a detailed overview how these operations can be handled with
ICP.
Subproject(s): T1

 Bibtex
 PDF open 
 [Fränzle et al.,
2015]
 Martin Fränzle, Sebastian Gerwinn, Paul Kröger,
Alessandro Abate, and JoostPieter Katoen.
Multiobjective parameter synthesis in probabilistic hybrid systems.
In Sriram Sankaranarayanan and Enrico Vicario, editors, Formal Modeling
and Analysis of Timed Systems, volume 9268 of Lecture Notes in
Computer Science, pages 93107. Springer International Publishing,
2015.
Abstract (click to open/close) Technical systems interacting with
the real world can be elegantly modelled using probabilistic hybrid automata
(PHA). Parametric probabilistic hybrid automata are dynamical systems
featuring hybrid discretecontinuous dynamics and parametric probabilistic
branching, thereby generalizing PHA by capturing a family of PHA within a
single model. Such system models have a broad range of applications, from
control systems over network protocols to biological components. We present a
novel method to synthesize parameter instances (if such exist) of PHA
satisfying a multiobjective bounded horizon specification over expected
rewards. Our approach combines three techniques: statistical model checking
of model instantiations, a symbolic version of importance sampling to handle
the parametric dependence, and SATmodulo theory solving for finding feasible
parameter instances in a multiobjective setting. The method provides
statistical guarantees on the synthesized parameter instances. To illustrate
the practical feasibility of the approach, we present experiments showing the
potential benefit of the scheme compared to a naive parameter exploration
approach.
Subproject(s):
H1/2,H4

 Bibtex
 PDF open 
© Springer Verlag (see article at SpringerLink)
 [Gao and Fränzle,
2015]
 Yang Gao and Martin Fränzle.
A solving procedure for stochastic satisfiability modulo theories with
continuous domain.
In Quantitative Evaluation of Systems, volume 9259, pages
295311. Springer, 2015.
Subproject(s): H1/2

 Bibtex

© Springer Verlag (see article at SpringerLink)
 [Müllner et al.,
2015]
 Nils Müllner, Martin Fränzle, and Sibylle Fröschle.
Estimating the probability of a timely traffichazard warning via
simulation.
In Proceedings of the 48th Annual Symposium on Simulation
(AnSS2015), Washington DC, USA, April 2015. IEEE Computer Society
Press.
Abstract (click to open/close) Traffic flow simulation is exploited
for estimating the probability that a message  a hazard warning in this
case  is correctly transmitted to an approaching car in time, that is,
before overstepping a safety threshold. The results derived by simulation
provide valuable insights in the functional relation between the numerous
authoritative parameters and the reliability of timely message
reception.
Subproject(s):
H1/2

 Bibtex
 PDF restricted 
 [Zou et al., 2015]
 Liang
Zou, Martin Fränzle, Naijun Zhan, and Peter Nazier Mosaad.
Automatic stability and safety verification for delay differential
equations.
In Daniel Kroening and Corina Pasareanu, editors, Proc. of the 27th
International Conference on Computer Aided Verification (CAV 2015),
LNCS. Springer Verlag, to appear July 2015.
Abstract (click to open/close) Delay differential equations (DDEs)
arise naturally as models of, a.o., networked control systems, where the
communication delay in the feedback loop % between controlled system and
controller cannot always be ignored. Such delays can e.g.prompt
oscillations in otherwise stable feedback loops and thus cause severe
deterioration of control performance, invalidating both stability and safety
properties. Despite the omnipresence of feedback delays, stateexploratory
automatic verification methods have until now concentrated on ordinary
differential equations (and their piecewise extensions to hybrid state) only,
failing to address the effects of delays on system dynamics. We overcome this
problem by iterating bounded degree intervalbased Taylor overapproximations
of the timewise segments of the solution to a DDE, thereby identifying and
automatically analyzing the operator that yields the parameters of the Taylor
overapproximation for the next temporal segment from the current one. By
using constraint solving for analyzing the properties of this operator, we
obtain a procedure able to provide stability and safety certificates for a
simple class of DDEs.
Subproject(s):
H1/2,H4

 Bibtex
 PDF restricted 
© Springer Verlag (see article at SpringerLink)
 [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 120, 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
nondeterminism. 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 nondeterminism 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 subdomain. The nondeterminism 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 nondeterministic choice
involved.
Keywords: Statistical model checking;
Stochastic hybrid systems; Nondeterminism; SSMT Subproject(s):
H1/2

 Bibtex
 PDF restricted 
 [Mahdi and Fränzle,
2014]
 Ahmed Mahdi and Martin Fränzle.
Generalized craig interpolation for stochastic satisfiability modulo theory
problems.
In Joel Ouaknine and James Worrell, editors, Proceedings of the 8th
International Workshop on Reachability Problems, RP 2014, volume 8762
of Lecture Notes in Computer Science, pages 203215. Springer
International Publishing Switzerland, 2014.
Abstract (click to open/close) Craig interpolation is widely used in
solving reachability and modelchecking problems by SAT or SMT techniques, as
it permits the computation of invariants as well as discovery of meaningful
predicates in CEGAR loops based on predicate abstraction. Extending such
algorithms from the qualitative to the quantitative setting of probabilistic
models seems desirable. In 2012, [Teige et al.] succeeded to define an
adequate notion of generalized, stochastic interpolants and to expose an
algorithm for efficiently computing them for stochastic Boolean
satisfiability problems, i.e., SSAT. In this work we present a notion of
Generalized Craig Interpolant for the stochastic SAT modulo theories
framework, i.e., SSMT, and introduce a mechanism to compute such stochastic
interpolants for nonpolynomial SSMT problems based on a sound and, w.r.t.
the arithmetic reasoner, relatively complete resolution calculus. The
algorithm computes interpolants in SAT, SMT, SSAT, and SSMT problems. As this
extends the scope of SSMTbased modelchecking of probabilistic hybrid
automata from the bounded to the unbounded case, we demonstrate our
interpolation principle on an unbounded probabilistic reachability problem in
a probabilistic hybrid automaton.
Subproject(s):
H4

 Bibtex
 PDF open 
© Springer Verlag (see article at SpringerLink)
 [Mahdi et al.,
2014]
 Ahmed Mahdi, Bernd Westphal, and Martin Fränzle.
Transformations for compositional verification of assumptioncommitment
properties.
In Joel Ouaknine and James Worrell, editors, Proceedings of the 8th
International Workshop on Reachability Problems, RP 2014, volume 8762
of Lecture Notes in Computer Science. Springer International
Publishing Switzerland, 2014.
Abstract (click to open/close) This paper presents a
transformationbased compositional verification approach for verifying
assumptioncommitment properties. Our approach improves the verification
process by pruning the state space of the model where the assumption is
violated. This exclusion is performed by transformation functions which are
defined based on a new notion of edges supporting a property. Our approach
applies to all computational models where an automaton syntax with locations
and edges induces a transition system semantics in a consistent way which is
the case for hybrid, timed, Buechi, and finite automata. We have successfully
applied our approach to Fischer's
protocol.
Subproject(s):
H1/2,R1,S2

 Bibtex
 PDF open 
© Springer Verlag (see article at SpringerLink)
 [Müllner et al.,
2014a]
 Nils Müllner, Oliver Theel, and Martin Fränzle.
Combining decomposition and lumping to evaluate semihierarchical
systems.
In Proceedings of the 28th IEEE International Conference on Advanced
Information Networking and Applications (AINA2014), pages 1049 
1056. IEEE, May 2014.
Abstract (click to open/close) Determining performance and fault
tolerance properties of distributed systems is a challenging task. One common
approach to quantify such properties is to construct the state space and the
transition model of the distributed system that is to be evaluated. The
challenge lies in the state space being exponentially large in the size of
the system. One popular approach to tackle this challenge is to combine
decomposition and lumping. The system is decomposed, the transition models of
the subsystems are constructed and minimized by lumping bisimilar states
under an equivalence relation, and the intermediate marginal transition
systems are composed to construct the minimal aggregate transition model. The
approach allows to circumvent the necessity to construct the full transition
model while preserving the ability to compute precise measures. The
decomposition yet hinges on the structure of the communication within the
system. When processes do not influence each other, decomposition is trivial
as it is arbitrary. On the contrary, when all processes are influenced by all
other processes  known as heterarchical structure  systems cannot
be decomposed at all. Between systems of independent and heterarchical
processes are i) hierarchically structured systems and ii) systems that are
globally hierarchical, but contain locally heterarchical subsystems. The
hierarchical type has been addressed previously. This paper targets the
second type  referred to as semihierarchically structured , thus
expanding the frontier from decomposing purely hierarchically structured
systems to decomposing semihierarchically structured systems. Furthermore,
this paper points out the role of different types of execution semantics
regarding the decomposition.
Subproject(s):
H4

 Bibtex
 PDF open 
 [Müllner et al.,
2014b]
 Nils Müllner, Oliver Theel, and Martin Fränzle.
Composing thermostatically controlled loads to determine the reliability
against blackouts.
In Proceedings of the 10th International Symposium on Frontiers of
Information Systems and Network Applications (FINA2014), pages 334 
341. IEEE, May 2014.
Abstract (click to open/close) Power grids are parallel systems in
which consumers demand a shared resource independent of each other. A
blackout occurs when the total demand increases or decreases too rapidly.
This paper combines methods and concepts from three domains. The first stems
from estimating the power consumption based on thermostatically controlled
loads via Markov chains. The second domain provides the composition of
parallel systems enriched by intermediate lumping to construct a minimal
aggregate transition model, in this case of a community of housings. The
third domain provides reasoning about fault tolerance properties by
introducing limiting window reliability as measure, suitable to account for
the continuous risk of blackouts. Combined, the three methods and concepts
allow to determine the risk of blackout of a community over
time.
Subproject(s): H4

 Bibtex
 PDF open 
 [Müllner et al.,
2013]
 Nils Müllner, Oliver Theel, and Martin Fränzle.
Combining decomposition and reduction for state space analysis of a
selfstabilizing system.
Journal of Computer and System Sciences (JCSS), 79(7):11131125,
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 wellknown 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 selfstabilizing 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 discretecontinuous 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 VNODELP, as a stateoftheart interval solver
for ODEs, and with bracketing systems, which exploit monotonicity properties
allowing to find enclosures for problems that VNODELP alone cannot enclose
tightly. We apply the combined iSATODE solver to the analysis of a variety
of nonlinear 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
newlydesigned conveyor belt system that combines hybrid behavior of parallel
components, a slipstick friction model with nonlinear dynamics and flow
invariants and several dimensions of parameterization. In the paper, we also
present and evaluate an extension of VNODELP tailored to its use as a
deduction mechanism within iSATODE, to allow fast reevaluations of
enclosures over arbitrary subranges of the analyzed time
span.
Keywords: Analysis of hybrid
discretecontinuous systems; Satisfiability modulo theories; Enclosure
methods for ODEs; Bracketing systems Subproject(s):
H1/2

 Bibtex
 PDF restricted 
 [Eggers et al.,
2012b]
 Andreas Eggers, Nacim Ramdani, Nedialko S. Nedialkov,
and Martin Fränzle.
Setmembership estimation of hybrid systems via SAT modulo ODE.
In Michel Kinnaert, editor, Proceedings of the 16th IFAC Symposium on
System Identification, pages 440445. The International Federation of
Automatic Control (IFAC), 2012.
Abstract (click to open/close) Set membership estimation (SME) of
nonlinear hybrid systems is still a challenging issue. Although SME of
nonlinear continuous systems has made significant progress recently, the
direct extension of these methods to the hybrid case is not easy. Meanwhile,
satisfiability (SAT) checkers for Boolean combinations of arithmetic
constraints over real and integervalued variables have made significant
progress, as they can effectively deal with algebraic constraints between
variables and nonlinear ODEs, what is denoted as SAT Modulo ODE. Finally,
the corresponding solvers solve in a natural way the hybrid differential and
algebraic constraints satisfaction problems that underlie SME of hybrid
systems. This paper presents the application of such a SAT Modulo ODE solver
to SME of hybrid dynamical
systems.
Subproject(s):
H1/2

 Bibtex
 PDF restricted 
 [Müllner et al.,
2012]
 Nils Müllner, Oliver Theel, and Martin Fränzle.
Combining decomposition and reduction for state space analysis of a
selfstabilizing system.
In Proceedings of the 2012 IEEE 26th International Conference on Advanced
Information Networking and Applications, AINA'12, page 8. IEEE
Computer Society, IEEE Computer Society, March 2012.
Best Paper Award.
Abstract (click to open/close) Verifying fault tolerance properties
of a distributed system can be achieved by state space analysis via Markov
chains. Yet, the power of such exact analytic methods is very limited as the
state space is exponentially proportional to the system size. We propose a
method that alleviates this limit. Lumping is a well known reduction
technique that can be applied to a Markov chain to prune redundant
information. We propose a system decomposition to employ lumping piecewise on
the considerably smaller Markov chains of the subsystems which are much more
likely to be tractable. Recomposing the lumped Markov chains of the
subsystems results in a configuration space that is likely to be considerably
smaller. An example demonstrates how the limiting window availability (i.e. a
fault tolerance property) can be computed for a system while exploiting the
combination of lumping and
decomposition.
Subproject(s):
H4

 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):132, 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
interpolationbased 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 
 [Dinh et al.,
2011]
 Nam Thang Dinh, Martin Fränzle, and Andreas Eggers.
AVACS H1/2 8year benchmark: Analyzing traffic models with iSAT.
AVACS Technical Report No. 81, SFB/TR 14 AVACS, July 2011.
ISSN: 18609821, http://www.avacs.org.
Abstract (click to open/close) In this technical report, we present
an application of the iSAT constraint solver to instances of traffic flow
networks.We give an account of the underlying model and provide details of
different instances of the model and a variety of verification and
falsification tasks handled by our
solver.
Subproject(s):
H1/2

 Bibtex
 PDF open 
 [Eggers et al.,
2011b]
 Andreas Eggers, Nacim Ramdani, Nedialko S. Nedialkov,
and Martin Fränzle.
Improving SAT modulo ODE for hybrid systems analysis by combining
different enclosure methods.
In Gilles Barthe, Alberto Pardo, and Gerardo Schneider, editors,
Proceedings of the Ninth International Conference on Software
Engineering and Formal Methods (SEFM), volume 7041 of
LNCS, pages 172187. Springer, 2011.
Abstract (click to open/close) Aiming at automatic verification and
analysis techniques for hybrid systems, we present a novel combination of
enclosure methods for ordinary differential equations (ODEs) with the iSAT
solver for Boolean combinations of arithmetic constraints. Improving on our
previous work, the contribution of this paper lies in combining iSAT with
VNODELP, as a stateoftheart enclosure method for ODEs, and with
bracketing systems whichby exploiting monotonicity properties of the
systemallow finding enclosures for problems that VNODELP alone cannot
enclose tightly. We apply our method to the analysis of a nonlinear hybrid
system by solving predicative encodings of an inductive stability argument
and evaluate the impact of different methods and their interplay in
combination.
Subproject(s):
H1/2

 Bibtex
 PDF restricted 
© Springer Verlag (see article at SpringerLink)
 [Fränzle and Lengauer,
2011]
 Martin Fränzle and Christian Lengauer.
Semantic independence.
In David Padua et al., editors, Encyclopedia of Parallel
Computing, pages 18031810. SpringerVerlag, sep 2011.
Subproject(s): R1

 Bibtex
 PDF
restricted 
© Springer Verlag (see article at SpringerLink)
 [Fränzle et al.,
2011]
 Martin Fränzle, Ernst Moritz Hahn, Holger Hermanns,
Nicolas Wolovick, and Lijun Zhang.
Measurability and safety verification for stochastic hybrid systems.
In Proceedings of the 14th international conference on Hybrid systems:
computation and control, HSCC '11, pages 4352, New York, NY, USA,
2011. ACM.
Abstract (click to open/close) Dealing with the interplay of
randomness and continuous time is important for the formal verification of
many real systems. Considering both facets is especially important for
wireless sensor networks, distributed control applications, and many other
systems of growing importance. An important traditional design and
verification goal for such systems is to ensure that unsafe states can never
be reached. In the stochastic setting, this translates to the question
whether the probability to reach unsafe states remains tolerable. In this
paper, we consider stochastic hybrid systems where the continuoustime
behaviour is given by differential equations, as for usual hybrid systems,
but the targets of discrete jumps are chosen by probability distributions.
These distributions may be general measures on state sets. Also
nondeterminism is supported, and the latter is exploited in an abstraction
and evaluation method that establishes safe upper bounds on reachability
probabilities. To arrive there requires us to solve semantic intricacies as
well as practical problems. In particular, we show that measurability of a
complete system follows from the measurability of its constituent parts. On
the practical side, we enhance tool support to work effectively on such
general models. Experimental evidence is provided demonstrating the
applicability of our approach on three case studies, tackled using a
prototypical implementation.
Keywords:
measurability, nondeterministic markov process, probabilistic hybrid
automaton, reachability, stochastic hybrid automaton Subproject(s):
H4

 Bibtex
 PDF restricted 
 [Kupferschmid et al.,
2011a]
 Stefan Kupferschmid, Bernd Becker, Tino Teige, and
Martin Fränzle.
Proof certificates and nonlinear arithmetic constraints.
In Proceedings of the 14th IEEE Symposium on Design and Diagnostics of
Electronic Circuits and Systems (DDECS 2011). IEEE, 2011.
Abstract (click to open/close) Symbolic methods in computeraided
verification rely heavily on constraint solvers. The correctness and
reliability of these solvers are of vital importance in the analysis of
safetycritical systems, e.g., in the automotive context. Satisfiability
results of a solver can usually be checked by probing the computed solution.
This is in general not the case for unsatisfiability results. In this paper,
we propose a certification method for unsatisfiability results for mixed
Boolean and nonlinear arithmetic constraint formulae. Such formulae arise in
the analysis of hybrid discrete/continuous systems. Furthermore, we test our
approach by enhancing the iSAT constraint solver to generate unsatisfiability
proofs, and implemented a tool that can efficiently validate such proofs.
Finally, some experimental results showing the effectiveness of our
techniques are given.
Subproject(s):
H1/2

 Bibtex
 PDF restricted 
 [Quesel et al.,
2011]
 J.D. Quesel, M. Fränzle, and W. Damm.
Crossing the bridge between similar games.
In Stavros Tripakis and Uli Fahrenberg, editors, Formal Modeling and
Analysis of Timed Systems  9th International Conference (FORMATS), Aalborg,
Denmark, 2123 September, 2011. Proceedings, Lecture Notes in Computer
Science (LNCS). SpringerVerlag, Sep. 2011.
15 pp. Accepted for publication on 8 July 2011.
Abstract (click to open/close) Specifications and implementations of
complex physical systems tend to differ as low level effects such as sampling
are often ignored when high level models are created. Thus, the low level
models are often not exact refinements of the high level specification.
However, they are similar to those. To bridge the gap between those models,
we study robust simulation relations for hybrid systems. In this paper, we
identify a family of robust simulation relations that allow for certain
bounded deviations in the behavior of a system specification and its
implementation in both values of the system variables and timings. We show
that for this relaxed version of simulation a broad class of logical
properties is preserved. The question whether two systems are in simulation
relation can be reduced to a reach avoid problem for hybrid games. We provide
a sufficient condition under which a winning strategy for these games
exists.
Subproject(s):
H1/2,H3

 Bibtex
 PDF restricted 
© Springer Verlag (see article at SpringerLink)
 [Teige and Fränzle,
2011a]
 Tino Teige and Martin Fränzle.
Generalized Craig interpolation for stochastic Boolean satisfiability
problems.
AVACS Technical Report No. 67, SFB/TR 14 AVACS, 2011.
ISSN: 18609821, http://www.avacs.org.
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 bounded
model checking (BMC) of symbolically represented Markov decision processes.
This paper identifies a notion of Craig interpolant for the SSAT
framework and develops an algorithm for computing such interpolants based on
SSAT resolution. As a potential application, we address the use of
interpolation in SSATbased BMC, turning the falsification procedure into a
verification approach for probabilistic safety
properties.
Subproject(s):
H1/2,H4

 Bibtex
 PDF open 
 [Teige and Fränzle,
2011b]
 Tino Teige and Martin Fränzle.
Generalized Craig interpolation for stochastic Boolean satisfiability
problems.
In Parosh Aziz Abdulla and K. Rustan M. Leino, editors, Proceedings of
the 17th International Conference on Tools and Algorithms for the
Construction and Analysis of Systems, volume 6605 of
LNCS, pages 158172. Springer, 2011.
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 bounded
model checking (BMC) of symbolically represented Markov decision processes.
This paper identifies a notion of Craig interpolant for the SSAT framework
and develops an algorithm for computing such interpolants based on SSAT
resolution. As a potential application, we address the use of interpolation
in SSATbased BMC, turning the falsification procedure into a verification
approach for probabilistic safety
properties.
Subproject(s):
H1/2,H4

 Bibtex
 PDF restricted 
© Springer Verlag (see article at SpringerLink)
 [Teige et al.,
2011]
 Tino Teige, Andreas Eggers, and Martin Fränzle.
Constraintbased analysis of concurrent probabilistic hybrid systems: An
application to networked automation systems.
Nonlinear Analysis: Hybrid Systems, 5(2):343366, 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
SSMTbased 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):436466, 2010.
Abstract (click to open/close) In this article, we recall different
approaches to the constraintbased, symbolic analysis of hybrid
discretecontinuous systems and combine them to a technology able to address
hybrid systems exhibiting both nondeterministic and probabilistic behavior
akin to infinitestate Markov decision processes. To enable mechanized
analysis of such systems, we extend the reasoning power of arithmetic
satisfiabilitymodulotheories (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 Booleanarithmetic constraint system.
This provides the technological basis for a constraintbased analysis of
densetime probabilistic hybrid automata, extending previous results
addressing discretetime automata (1). Generalizing SMTbased bounded
modelchecking of hybrid automata (2; 3), stochastic SMT including ODEs
permits the direct analysis of probabilistic bounded reachability problems of
densetime probabilistic hybrid automata without resorting to approximation
by intermediate finitestate
abstractions.
Keywords: Probabilistic hybrid
automata, bounded model checking, arithmetic constraint solving, stochastic
satisfiability Subproject(s): H1/2,H4

 Bibtex
 PDF restricted 
 [Fränzle et al.,
2010b]
 Martin Fränzle, Tino Teige, and Andreas Eggers.
Satisfaction meets expectations: Computing expected values of probabilistic
hybrid systems with smt.
In Dominique Mery and Stephan Merz, editors, Integrated Formal Methods
2010, volume 6396 of Lecture Notes in Computer Science
(LNCS), pages 168182. Springer, 2010.
Abstract (click to open/close) Stochastic satisfiability modulo
theories (SSMT), which is an extension of satisfiability modulo theories with
randomized quantification, has successfully been used as a symbolic technique
for computing reachability probabilities in probabilistic hybrid systems.
Motivated by the fact that several industrial applications call for
quantitative measures that go beyond mere reachability probabilities, this
paper extends SSMT to compute expected values of probabilistic hybrid systems
like, e.g., meantimes to failure. Practical applicability of the proposed
approach is demonstrated by a case study from networked automation
systems.
Subproject(s):
H1/2,H4

 Bibtex
 PDF restricted 
© Springer Verlag (see article at SpringerLink)
 [Teige and Fränzle,
2010]
 Tino Teige and Martin Fränzle.
Resolution for stochastic Boolean satisfiability.
In Christian Fermüller and Andrei Voronkov, editors, Logic for
Programming, Artificial Intelligence, and Reasoning, 17th International
Conference (LPAR17), volume 6397 of Logic for Programming,
Artificial Intelligence, and Reasoning, pages 625639.
SpringerVerlag, 2010.
Abstract (click to open/close) The stochastic Boolean satisfiability
(SSAT) problem was introduced by Papadimitriou in 1985 by adding a
probabilistic model of uncertainty to propositional satisfiability through
randomized quantification. SSAT has many applications, e.g., in probabilistic
planning and, more recently by integrating arithmetic, in probabilistic model
checking. In this paper, we first present a new result on the computational
complexity of SSAT: SSAT remains PSPACEcomplete even for its restriction to
2CNF. Second, we propose a sound and complete resolution calculus for SSAT
complementing the classical backtracking search
algorithms.
Subproject(s):
H1/2,H4

 Bibtex
 PDF restricted 
© Springer Verlag (see article at SpringerLink)
 [Á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 301315, 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
firstorder 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 
 [Eggers et al., 2009a]
 Andreas Eggers, Martin
Fränzle, and Christian Herde.
Application of constraint solving and odeenclosure methods to the analysis
of hybrid systems.
In Theodore E. Simos, George Psihoyios, and Ch. Tsitouras, editors,
NUMERICAL ANALYSIS AND APPLIED MATHEMATICS: International Conference on
Numerical Analysis and Applied Mathematics 2009, volume 1168 of
American Institue of Physics (AIP) Conference Proceedings, pages
13261330, Melville, New York, 2009. American Institue of Physics.
copyright American Institute of Physics.
Abstract (click to open/close) In this short paper, we summarize our
approach to analyzing hybrid discretecontinuous systems by reduction to
constraint solving paired with enclosure methods for sets of initial value
problems of ordinary differential
equations.
Keywords: hybrid discretecontinuous
systems, verification, ordinary differential equations, constraint solving,
PACS: 02.60.Lj, 02.70.c, 89.75.k Subproject(s):
H1/2

 Bibtex
 PDF open 
 [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(23):171196, 2009.
Abstract (click to open/close) Duration Calculus (abbreviated to DC)
is an intervalbased, metrictime temporal logic designed for reasoning about
embedded realtime 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 nonelementary 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 pointbased temporal logics, where
lineartime problems are safely approximated by branchingtime counterparts
amenable to more efficient modelchecking algorithms. Mimicking the role that
a situation has in (A)CTL as the origin of a set of linear traces, we define
a branchingtime counterpart to intervalbased temporal logics building on
situation pairs spanning sets of intervals. While this branchingtime
interval semantics yields the desired reduction in complexity of the
modelchecking 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 4fold
exponential modelchecking problem sufficiently accurately approximating the
original one. Furthermore, when chop occurs in negative polarity only in DC
formulas, we have a doubly exponential modelchecking
algorithm.
Subproject(s):
R1

 Bibtex
 PDF restricted 
 [Fränzle and
Swaminathan, 2009]
 Martin Fränzle and Mani Swaminathan.
Revisiting decidability and optimum reachability for multipriced timed
automata.
In J. Ouaknine and F. Vaandrager, editors, The 7th International
Conference on Formal Modelling and Analysis of Timed Systems (FORMATS
2009), volume 5813 of Lecture Notes in Computer Science
(LNCS), pages 149163. Springer, September 2009.
Abstract (click to open/close) We investigate the optimum
reachability problem for MultiPriced Timed Automata (MPTA) that admit both
positive and negative costs on edges and locations, thus bridging the gap
between the results of Bouyer et al. (2007) and of Larsen and Rasmussen
(2008). Our contributions are the following: (1) We show that even the
location reachability problem is undecidable for MPTA equipped with both
positive and negative costs, provided the costs are subject to a bounded
budget, in the sense that paths of the underlying MultiPriced Transition
System (MPTS) that operationally exceed the budget are considered as not
being viable. This undecidability result follows from an encoding of Stop
Watch Automata using such MPTA, and applies to MPTA with as few as two cost
variables, and even when no costs are incurred upon taking edges. (2) We then
restrict the MPTA such that each viable quasicyclic path of the underlying
MPTS incurs a minimum absolute cost. Under such a condition, the location
reachability problem is shown to be decidable and the optimum cost is shown
to be computable for MPTA with positive and negative costs and a bounded
budget. These results follow from a reduction of the optimum reachability
problem to the solution of a linear constraint system representing the path
conditions over a finite number of viable paths of bounded
length.
Subproject(s):
R1

 Bibtex
 PDF open 
© Springer Verlag (see article at SpringerLink)
 [Fränzle et al.,
2009]
 Martin Fränzle, Andreas Eggers, Christian Herde, and
Tino Teige.
Hybrid discretecontinuous systems.
In Modern Computational Science 09, pages 363378. BISVerlag der
Carl von Ossietzky Universität Oldenburg, 2009.
Subproject(s): H1/2

 Bibtex
 PDF restricted 
 [Heise et al.,
2009]
 William Pihl Heise, Michael R. Hansen, and Martin
Fränzle.
A prototype of a model checker for duration calculus.
In Proceedings of the 21st Nordic Workshop on Programming Theory, NWPT
'09, pages 2628, Kgs. Lyngby, Denmark, 2009. DTU Informatics,
Danmarks Tekniske Universitet.
Subproject(s): R1

 Bibtex

 [Kupferschmid et al.,
2009]
 Stefan Kupferschmid, Tino Teige, Bernd Becker, and Martin
Fränzle.
Proofs of unsatisfiability for mixed boolean and nonlinear arithmetic
constraint formulae.
In Carsten Gremzow and Nico Moser, editors, Proceedings of the 12th
Workshop ``Methoden und Beschreibungssprachen zur Modellierung und
Verifikation von Schaltungen und Systemen'' (MBMV 2009), pages 2736.
Universitätsverlag TU Berlin, 2009.
Abstract (click to open/close) Symbolic methods in computeraided
verification rely on appropriate constraint solvers. Correctness and
reliability of solvers are a vital requirement in the analysis of
safetycritical systems, e.g., in the automotive context. Satisfiability
results of a solver can usually be checked by probing the computed solution.
However, efficient validation of an uncertified unsatisfiability result for
some constraint formula is nearly impossible. In this paper, we propose a
certification method for unsatisfiability results for mixed Boolean and
nonlinear arithmetic constraint formulae. Such formulae arise in the
analysis of hybrid discretecontinuous
systems.
Subproject(s):
H1/2

 Bibtex
 PDF restricted 
 [Teige and Fränzle,
2009]
 Tino Teige and Martin Fränzle.
Constraintbased analysis of probabilistic hybrid systems.
In A. Giua, C. Mahulea, M. Silva, and J. Zaytoon, editors, Proceedings of
the 3rd International Federation of Automatic Control (IFAC) Conference on
Analysis and Design of Hybrid Systems (ADHS 2009), pages 162167.
International Federation of Automatic Control (IFAC), 2009.
Abstract (click to open/close) Aiming at fully symbolic methods for
the analysis of probabilistic hybrid systems, we recently introduced the
notion of stochastic satisfiability modulo theories (SSMT) problems and the
corresponding SiSAT solving algorithm. The notion of SSMT extends SMT with
randomized (aka. stochastic) as well as existential and universal
quantification as known from stochastic propositional satisfiability. In this
paper, we describe the symbolic encoding of scheduledevent probabilistic
hybrid automata by means of a case study from the networked automation system
domain. We furthermore report on the SSMT solver SiSAT including recent
enhancements in terms of solver performance, expressiveness of the input
language, and handling of numerical issues. The significance of the
performance enhancements is demonstrated by empirical
results.
Keywords: Probabilistic hybrid systems,
probabilistic logic, constraint satisfaction problems, problem solvers,
automatic verification Subproject(s):
H1/2,H4

 Bibtex
 PDF restricted 
 [Eggers et al.,
2008b]
 Andreas Eggers, Martin Fränzle, and Christian Herde.
SAT modulo ODE: A direct SAT approach to hybrid systems.
AVACS Technical Report No. 37, Sonderforschungsbereiche (SFB)/ Transregio (TR)
14 AVACS, April 2008.
ISSN: 18609821, http://www.avacs.org.
Abstract (click to open/close) In order to facilitate automated
reasoning about large Boolean combinations of nonlinear arithmetic
constraints involving ordinary differential equations (ODEs), we provide a
seamless integration of safe numeric overapproximation of initialvalue
problems into a SATmodulotheory (SMT) approach to intervalbased arithmetic
constraint solving. Intervalbased safe numeric approximation of ODEs is used
as an interval contractor being able to narrow candidate sets in phase space
in both temporal directions: postimages of ODEs (i.e., sets of states
reachable from a set of initial values) are narrowed based on partial
information about the initial values and, vice versa, preimages are narrowed
based on partial knowledge about postsets. In contrast to the related CLP(F)
approach of Hickey and Wittenberg, we do (a) support coordinate
transformations mitigating the wrapping effect encountered upon iterating
intervalbased overapproximations of reachable state sets and (b) embed the
approach into an SMT framework, thus accelerating the solving process through
the algorithmic enhacements of recent SAT solving
technology.
Subproject(s):
H1/2

 Bibtex
 PDF open 
 [Eggers et al.,
2008c]
 Andreas Eggers, Martin Fränzle, and Christian Herde.
SAT modulo ODE: A direct SAT approach to hybrid systems.
In Sungdeok (Steve) Cha, JinYoung Choi, Moonzoo Kim, Insup Lee, and Mahesh
Viswanathan, editors, Proceedings of the 6th International Symposium on
Automated Technology for Verification and Analysis (ATVA'08), volume
5311 of Lecture Notes in Computer Science (LNCS), pages
171185. SpringerVerlag, 2008.
Abstract (click to open/close) In order to facilitate automated
reasoning about large Boolean combinations of nonlinear arithmetic
constraints involving ordinary differential equations (ODEs), we provide a
seamless integration of safe numeric overapproximation of initialvalue
problems into a SATmodulotheory (SMT) approach to intervalbased arithmetic
constraint solving. Intervalbased safe numeric approximation of ODEs is used
as an interval contractor being able to narrow candidate sets in phase space
in both temporal directions: postimages of ODEs (i.e., sets of states
reachable from a set of initial values) are narrowed based on partial
information about the initial values and, vice versa, preimages are narrowed
based on partial knowledge about postsets. In contrast to the related CLP(F)
approach of Hickey and Wittenberg, we do (a) support coordinate
transformations mitigating the wrapping effect encountered upon iterating
intervalbased overapproximations of reachable state sets and (b) embed the
approach into an SMT framework, thus accelerating the solving process through
the algorithmic enhancements of recent SAT solving
technology.
Subproject(s):
H1/2

 Bibtex
 PDF restricted 
© Springer Verlag (see article at SpringerLink)
 [Fränzle,
2008]
 Martin Fränzle.
Engineering constraint solvers for the analysis of hybrid systems.
In 20th Nordic Workshop on Programming Theory, NWPT '08, pages
436466. Institute of Cybernetics, Tallinn Technical University, 2008.
Subproject(s): H1/2,H4

 Bibtex

 [Fränzle and Hansen,
2008]
 Martin Fränzle and Michael R. Hansen.
Efficient model checking for duration calculus based on branchingtime
approximations.
In Antonio Cerone and Stefan Gruner, editors, Proceedings of the 6th
Institute of Electrical and Electronics Engineers (IEEE) International
Conferences on Software Engineering and Formal Methods (SEFM 08),
pages 6372. Institute of Electrical and Electronics Engineers (IEEE)
Computer Society Press, 2008.
Abstract (click to open/close) Duration Calculus (abbreviated to DC)
is an intervalbased, metrictime temporal logic designed for reasoning about
embedded realtime 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 nonelementary and thus impractical. We here
investigate a similar approximation as frequently employed in model checking
situationbased temporal logics, where lineartime problems are safely
approximated by branchingtime counterparts amenable to more efficient
modelchecking algorithms. Mimicking the role that a situation has in (A)CTL
as origin of a set of linear traces, we define a branchingtime counterpart
to intervalbased temporal logics building on situation pairs spanning sets of
intervals. While this branchingtime interval semantics yields the desired
reduction in complexity of the modelchecking problem, from nonelementary 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 4fold exponential modelchecking problem
sufficiently accurately approximating the original
one.
Subproject(s): R1

 Bibtex
 PDF restricted 
 [Fränzle et al.,
2008a]
 M. Fränzle, H. Hermanns, and T. Teige.
Stochastic satisfiability modulo theory: A novel technique for the analysis
of probabilistic hybrid systems.
In Magnus Egerstedt and Bud Mishra, editors, Proceedings of the 11th
International Conference on Hybrid Systems: Computation and Control
(HSCC'08), volume 4981 of Lecture Notes in Computer Science
(LNCS), pages 172186. Springer, 2008.
Abstract (click to open/close) The analysis of hybrid systems
exhibiting probabilistic behaviour is notoriously difficult. To enable
mechanised analysis of such systems, we extend the reasoning power of
arithmetic satisfiabilitymodulotheory solving (SMT) by a comprehensive
treatment of randomized (a.k.a. stochastic) quantification over discrete
variables within the mixed Booleanarithmetic constraint system. This provides
the technological basis for a fully symbolic analysis of probabilistic hybrid
automata. Generalizing SMTbased bounded modelchecking of hybrid automata
[2, 11], stochastic SMT permits the direct and fully symbolic analysis of
probabilistic bounded reachability problems of probabilistic hybrid automata
without resorting to approximation by intermediate finitestate
abstractions.
Subproject(s):
H1/2,H4

 Bibtex
 PDF restricted 
© Springer Verlag (see article at SpringerLink)
 [Fränzle et al.,
2008b]
 M. Fränzle, H. Hermanns, and T. Teige.
Stochastic satisfiability modulo theory: A novel technique for the analysis
of probabilistic hybrid systems.
In Magnus Egerstedt and Bud Mishra, editors, PreProceedings of the
European Joint Conferences on Theory and Practice of Software (ETAPS) 2008
Sixth Workshop on Quantitative Aspects of Programming Languages (QAPL
2008), volume 4981 of Lecture Notes in Computer Science
(LNCS), pages 172186. SpringerVerlag, 2008.
Extended abstract.
Abstract (click to open/close) The analysis of hybrid systems
exhibiting probabilistic behaviour is notoriously difficult. To enable
mechanised analysis of such systems, we extend the reasoning power of
arithmetic satisfiabilitymodulotheory solving (SMT) by a comprehensive
treatment of randomized (a.k.a. stochastic) quantification over discrete
variables within the mixed Booleanarithmetic constraint system. This
provides the technological basis for a fully symbolic analysis of
probabilistic hybrid automata. Generalizing SMTbased bounded modelchecking
of hybrid automata [2,9], stochastic SMT permits the direct and fully
symbolic analysis of probabilistic bounded reachability problems of
probabilistic hybrid automata without resorting to approximation by
intermediate finitestate abstractions.
Keywords:
Stochastic satisfiability, infinite domains, probabilistic hybrid automata,
probabilistic bounded reachability. Subproject(s):
H1/2,H4

 Bibtex
 PDF open 
© Springer Verlag (see article at SpringerLink)
 [Herde et al.,
2008]
 C. Herde, A. Eggers, M. Fränzle, and T. Teige.
Analysis of hybrid systems using HySAT.
In The Third International Conference on Systems (ICONS 2008),
pages 196201. Institute of Electrical and Electronics Engineers (IEEE)
Computer Society, 2008.
Abstract (click to open/close) In this paper we describe the
complete workflow of analyzing the dynamic behavior of safetycritical
embedded systems with HySAT. HySAT is an arithmetic constraint solver with a
tightly integrated bounded model checker for hybrid discretecontinuous
systems which  in contrast to many other solvers  is not confined to linear
arithmetic, but can also deal with nonlinear constraints involving
transcendental functions. Based on a controller for train separation
implementing a "moving block" interlocking scheme in the forthcoming European
Train Control System Level 3, we exemplify the usage of the tool over the
whole cycle from encoding a hybrid system to interpreting the
results.
Subproject(s):
H1/2

 Bibtex
 PDF restricted 
 [Kupferschmid et al.,
2008c]
 Stefan Kupferschmid, Tino Teige, Bernd Becker, and
Martin Fränzle.
Proofs of unsatisfiability for mixed boolean and nonlinear arithmetic
constraint formulae.
AVACS Technical Report No. 40, Sonderforschungsbereiche (SFB)/ Transregio (TR)
14 AVACS, June 2008.
ISSN: 18609821, http://www.avacs.org.
Abstract (click to open/close) In recent years, the use of
constraint solvers for analysis and verification of industrial systems has
become increasingly popular. The correctness and reliability of the results
returned by the employed solvers are a vital requirement, in particular for
safetycritical systems. If a solver proves the satisfiability of a
constraint system and returns a solution then the answer of the solver can be
validated by means of the solution. However, in case the solver claims that
the constraint system is unsatisfiable without any certificate then the
validation of this answer is not that simple. In this paper, we establish the
theoretical basis of generating proofs of unsatisfiability in the mixed
Boolean and nonlinear arithmetic constraint framework over the reals and
integers. To do so, we propose a simple rulebased calculus for unsatisfiable
mixed Booleanarithmetic constraints to produce and check unsatisfiability
proofs. Furthermore, we enhance the iSAT constraint solver to generate
unsatisfiability proofs, we implement a tool validating such proofs, and give
some experimental results.
Subproject(s):
H1/2

 Bibtex
 PDF open 
 [Swaminathan
et al., 2008]
 Mani Swaminathan, Martin Fränzle, and
JoostPieter Katoen.
The surprising robustness of (closed) timed automata against
clockdrift.
In Giorgio Ausiello, Juhani Karhumäki, Giancarlo Mauri, and Luke Ong,
editors, The 5th International Federation for Information Processing
(IFIP) International Conference on Theoretical Computer Science (IFIP TCS
2008), volume 273, pages 537553. SpringerVerlag, September 2008.
Abstract (click to open/close) We investigate reachability (or
equivalently, safety) for timed systems modelled as Timed Automata (TA) under
notions of â€œrobustnessâ€?, i.e., when the clocks of the TA may drift
by small amounts. Our contributions are twofold: (1) We first consider the
model of clockdrift introduced by Puri [1] and subsequently studied in other
works [2,3,4]. We show that the standard zonebased forward reachability
analysis performed by tools such as UPPAAL is in fact exact for TA with
closed guards, invariants, and targets, when testing robust safety of timed
systems having an arbitrary, but finite lifetime. (2) Next, we consider a
more realistic model of drifting clocks that takes into account the regular
resynchronization performed in most practical systems. We then show that the
standard reachability analysis of tools like UPPAAL again suffices to test
for robust safety in this model of clockdrift, for TA with closed guards,
invariants, and targets, but now without any restrictions on system
lifetime.
Subproject(s):
R1

 Bibtex
 PDF open 
© Springer Verlag (see article at SpringerLink)
 [Teige and Fränzle,
2008]
 T. Teige and M. Fränzle.
Stochastic satisfiability modulo theories for nonlinear arithmetic.
In L. Perron and M. A. Trick, editors, Integration of AI and OR
Techniques in Constraint Programming for Combinatorial Optimization Problems,
5th International Conference, CPAIOR 2008, volume 5015 of
Lecture Notes in Computer Science (LNCS), pages 248262.
Springer, 2008.
Abstract (click to open/close) The stochastic satisfiability modulo
theories (SSMT) problem is a generalization of the SMT problem on existential
and randomized (aka. stochastic) quantification over discrete variables of an
SMT formula. This extension permits the concise description of diverse
problems combining reasoning under uncertainty with data dependencies.
Solving problems with various kinds of uncertainty has been extensively
studied in Artificial Intelligence. Famous examples are stochastic
satisfiability and stochastic constraint programming. In this paper, we
extend the algorithm for SSMT for decidable theories presented in [FHT08] to
nonlinear arithmetic theories over the reals and integers which are in
general undecidable. Therefore, we combine approaches from Constraint
Programming, namely the iSAT algorithm tackling mixed Boolean and nonlinear
arithmetic constraint systems, and from Artificial Intelligence handling
existential and randomized quantifiers. Furthermore, we evaluate our novel
algorithm and its enhancements on benchmarks from the probabilistic hybrid
systems domain.
Subproject(s):
H1/2,H4

 Bibtex
 PDF restricted 
© Springer Verlag (see article at SpringerLink)
 [Teige et al., 2008]
 Tino
Teige, Christian Herde, Martin Fränzle, and Erika Ábrahám.
Conflict analysis and restarts in a mixed boolean and nonlinear arithmetic
constraint solver.
AVACS Technical Report No. 34, Sonderforschungsbereiche (SFB)/ Transregio (TR)
14 AVACS, January 2008.
ISSN: 18609821, http://www.avacs.org.
Abstract (click to open/close) The recently presented constraint
solver HySAT tackles the in general undecidable problem of solving mixed
Boolean and nonlinear arithmetic constraint formulae over the reals
involving transcendental functions. The algorithmic core of HySAT is the iSAT
algorithm, a tight integration of the DavisPutnamLogemannLoveland
algorithm with interval constraint propagation enriched by enhancements like
conflictdriven clause learning and nonchronological backtracking. However,
it was an open question whether HySAT's conflict analysis scheme, an adapted
first unique implication point technique as applied in most modern SAT
solvers, performs favorably compared to other schemes. In this paper, we
compare several conflict analysis heuristics to answer this question.
Furthermore, we consider the integration of restarts into the iSAT algorithm
and investigate their impact. For our empirical results we use benchmarks
from the hybrid systems domain.
Subproject(s):
H1/2

 Bibtex
 PDF open 
 [Becker et al.,
2007a]
 Bernd Becker, Werner Damm, Martin Fränzle,
ErnstRüdiger Olderog, Andreas Podelski, and Reinhard Wilhelm.
SFB/TR 14 AVACS  automatic verification and analysis of complex
systems.
it  Information Technology, 49(2):118126, 2007.
http://itInformationTechnology.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 Hansen,
2007]
 Martin Fränzle and Michael R. Hansen.
Deciding an interval logic with accumulated durations.
In Orna Grumberg and Michael Huth, editors, Thirteenth International
Conference on Tools and Algorithms for the Construction and Analysis of
Systems (TACAS 07), volume 4424 of Lecture Notes in Computer
Science, pages 201215. Springer, 2007.
Abstract (click to open/close) A decidability result and a
modelchecking procedure for a rich subset of Duration Calculus (DC) [19] is
obtained through reductions to is obtained through reductions to Firstorder
logic over the realclosed field and to MultiPriced Timed Automata (MPTA)
[13]. In contrast to other reductions of fragments of DC to reachability
problems in timed automata, the reductions do also cover constraints on
positive linear combinations of accumulated durations. By being able to
handle accumulated durations under chop as well as in arbitrary positive
Boolean contexts, the procedures extend the results of Zhou et al. [22] on
decidability of linear duration invariants to a much wider fragment of
DC.
Keywords: Realtime systems, metrictime
temporal logic, decidability, modelchecking, multipriced timed
automata Subproject(s): H1

 Bibtex
 PDF restricted 
© Springer Verlag (see article at SpringerLink)
 [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:179198, 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 DPLLbased pseudoBoolean 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, infinitestate 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 nonlinear arithmetic constraint systems with
complex boolean structure.
Journal on Satisfiability, Boolean Modeling and Computation  Special
Issue on SAT/CP Integration, 1:209236, 2007.
Abstract (click to open/close) In order to facilitate automated
reasoning about large Boolean combinations of nonlinear arithmetic
constraints involving transcendental functions, we provide a tight
integration of recent SAT solving techniques with intervalbased 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 nonlinear 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 et al.,
2007b]
 Martin Fränzle, Hardi Hungar, Christian Schmitt, and
Boris Wirtz.
Hlang: Compositional representation of hybrid systems via predicates.
AVACS Technical Report No. 20, SFB/TR 14 AVACS, July 2007.
ISSN: 18609821, http://www.avacs.org.
Abstract (click to open/close) Given the structural diversity of
modeling paradigms for hybridsystems that are in widespread use, which ranges
from asignaltransducerbased view like in Simulink/Stateflow to
anautomatonbased view in various hybrid automata frameworks, there isneed
for an intermediatelevel language that can accommodate thesestructures in a
concise way, thereby isolating verification backendsfrom the particular
modeling frontend used.This technical report provides a description of the
intermediatelevelmodeling language for hybrid systems used in project area H
of AVACS asa gateway to verification
backends.
Subproject(s):
H1/2,H3

 Bibtex
 PDF open 
 [Swaminathan and Fränzle,
2007]
 Mani Swaminathan and Martin Fränzle.
A symbolic decision procedure for robust safety of timed systems.
In proceedings on the 14th International Symposium on Temporal
Representation and Reasoning (TIME 2007). IEEE CS Press, 2007.
To appear as a short paper/poster.
Abstract (click to open/close) We present a symbolic algorithm for
deciding safety (reachability) of timed systems modelled as Timed Automata
(TA), under the notion of robustness w.r.t infinitesimal clockdrift. The
algorithm uses a ``neighbourhood'' operator on zones that is efficient to
compute. In contrast to other approaches for robustly deciding reachability
of TA, which are either regionbased (Puri, 2000), (DeWulf, Doyen, Markey,
and Raskin, 2004), or involve a combination of forward and backward analyses
when zonebased (Daws and Kordy, 2006), ours is a zonebased fully forward
algorithm that is guaranteed to terminate, requires no special treatment of
cycles in TA, and can be applied to target states that need not be
closed.
Subproject(s):
H1

 Bibtex
 PDF restricted 
 [Teige et al.,
2007]
 Tino Teige, Christian Herde, Martin Fränzle, Natalia
Kalinnik, and Andreas Eggers.
A generalized twowatchedliteral scheme in a mixed boolean and nonlinear
arithmetic constraint solver.
In José Neves, Manuel Filipe Santos, and José Manuel Machado, editors,
Proceedings of the 13^{th} Portuguese Conference on Artificial
Intelligence (EPIA 2007), New Trends in Artificial Intelligence, pages
729741. APPIA, December 2007.
Abstract (click to open/close) In its combination with
conflictdriven clause learning the twowatchedliteral scheme led to
enormous performance gains in propositional SAT solving. The idea of this
approach is to accelerate the deduction phase of a SAT solver by saving a
high number of unnecessary and expensive computation steps originating in
visits of indefinite clauses. In this paper we give a detailed explanation of
the generalized watch scheme, called twowatchedatom scheme,
implemented in our intervalbased constraint solver HySAT, the latter being a
solver for mixed Boolean and nonlinear arithmetic constraint formulae. As
opposed to the purely Boolean setting, the more general form of atomic
formulae to be watched in our solver necessitates an extension of the
original scheme and calls for a careful design of the data structures
employed in the implementation. We present experimental results to
demonstrate the speedup obtained by the proposed
scheme.
Subproject(s): H1,
H2

 Bibtex
 PDF restricted 
 [Ábrahám et
al., 2006b]
 Erika Ábrahám, Tobias Schubert, Bernd
Becker, Martin Fränzle, and Christian Herde.
Parallel SAT solving in bounded model checking.
In Proc. of PDMC'06, Lecture Notes in Computer Science. Springer
Verlag, 2006.
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
firstorder 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.
Subproject(s):
H2

 Bibtex
 PDF restricted 
© Springer Verlag (see article at SpringerLink)
 [Badban et al.,
2006]
 Bahareh Badban, Martin Fränzle, Jan Peleska, and Tino
Teige.
Test automation for hybrid systems.
In Proceedings of the Third International Workshop on SOFTWARE QUALITY
ASSURANCE (SOQUA 2006), pages 1421, Portland Oregon, USA, November
2006.
Abstract (click to open/close) This article presents novel results
on automated test generation for hybrid control systems, which involves the
generation of both discrete and realvalued, potentially timecontinuous,
input data to the system under test. Our generation techniques are allocated
in two layers: The upper layer contains a symbolic test case generator
constructing test cases as paths through an abstracted representation model
of the system under test. Different test strategies designed to pursue
various quality objectives lead to different selections of symbolic test
cases. Symbolic test cases are transformed into feasible, i.e., executable,
test cases by constructing concrete sequences of input data, allowing the
execution of the preplanned transition sequence. The input data construction
is performed by the lower layer consisting of a constraint solver which
applies interval analysis techniques to identify the domains from where to
pick the appropriate test data. This process is made efficient by combining
subpaving with forwardbackward interval constraint propagation. On both
layers learning algorithms are applied in order to avoid the spending of
computation time on paths and subconstraints, respectively, which are
already known not to contribute to the
solution.
Subproject(s):
H1,H2

 Bibtex
 PDF restricted 
 [Fränzle et al.,
2006]
 Martin Fränzle, Christian Herde, Stefan Ratschan,
Tobias Schubert, and Tino Teige.
Interval constraint solving using propositional SAT solving
techniques.
In Proceedings of the CP 2006 First International Workshop on the
Integration of SAT and CP Techniques, pages 8195, 2006.
Abstract (click to open/close) In order to facilitate automated
reasoning about large Boolean combinations of nonlinear arithmetic
constraints involving transcendental functions, we extend the paradigm of
lazy theorem proving to intervalbased arithmetic constraint solving.
Algorithmically, our approach deviates substantially from "classical" lazy
theorem proving approaches in that it directly controls arithmetic constraint
propagation from the SAT solver rather than completely delegating arithmetic
decisions to a subordinate solver. From the constraint solving perspective,
it extends intervalbased constraint solving with all the algorithmic
enhancements that were instrumental to the enormous performance gains
recently achieved in propositional SAT solving, like conflictdriven learning
combined with nonchronological
backtracking.
Subproject(s):
H1,H2

 Bibtex
 PDF open 
 [Metzner et al.,
2006]
 A. Metzner, M. Fränzle, C. Herde, and I. Stierand.
An Optimal Approach to the Task Allocation Problem on Hierarchical
Architectures.
In Proceedings of the 20th IEEE International Parallel and Distributed
Processing Symposium. IEEE Computer Society, 2006.
Abstract (click to open/close) We present a SATbased approach to
the task and message allocation problem of distributed realtime systems with
hierarchical architectures. In contrast to the heuristic approaches usually
applied to this problem, our approach is guaranteed to find an optimal
allocation for realistic task systems running on complex target
architectures. Our method is based on the transformation of such scheduling
problems into nonlinear integer optimization problems. The core of the
numerical optimization procedure we use to discharge those problems is a
solver for arbitrary Boolean combinations of integer constraints. Optimal
solutions are obtained by imposing a binary search scheme on top of that
solver. Experiments show the applicability of our approach to industrialsize
task systems, which are mapped to heterogeneous hierarchical hardware
architectures.
Subproject(s):
R2,H2

 Bibtex
 PDF restricted 
 [Enslev et
al., 2005]
 Jacob Enslev, AnneSofie Nielsen, Martin
Fränzle, and Michael R. Hansen.
Bounded model construction for duration calculus.
In Neil Jones et al., editor, Proceedings of the 17th Nordic Workshop on
Programming Theory (NWPT 05). Københavns Universitet, October 2005.
Subproject(s): H1

 Bibtex
 PDF restricted 
 [Fränzle and Hansen,
2005]
 Martin Fränzle and Michael R. Hansen.
A robust interpretation of duration calculus.
In Proceedings of the International Colloquium on Theoretical Aspects of
Computing (ICTAC 05), volume 3722 of LNCS, pages
257271. Springer Verlag, 2005.
Abstract (click to open/close) We transfer the concept of robust
interpretation from arithmetic firstorder theories to metrictime temporal
logics. The idea is that the interpretation of a formula is robust if its
truth value does not change under small variation of the constants in the
formula. Exemplifying this on Duration Calculus (DC), our findings are that
the robust interpretation of DC is equivalent to a multivalued
interpretation that uses the real numbers as semantic domain and assigns
Lipschitzcontinuous interpretations to all operators of DC. Furthermore,
this continuity permits approximation between discrete and dense time, thus
allowing exploitation of discretetime (semi)decision procedures on
densetime properties.
Keywords: Metrictime
temporal logic; Robust interpretation; Discrete time vs. dense
time Subproject(s): H1

 Bibtex
 PDF restricted 
© Springer Verlag (see article at SpringerLink)
 [Metzner et al.,
2005]
 A. Metzner, M. Fränzle, C. Herde, and I. Stierand.
Scheduling Distributed RealTime Systems by Satisfiability Checking.
In Proceedings of the IEEE Conference on Embedded and RealTime Computing
Systems and Applications, pages 409415. IEEE Computer Society, 2005.
Abstract (click to open/close) We present a SATbased approach to
the task and message allocation problem of distributed realtime systems. In
contrast to the heuristic approaches usually applied to this problem, our
approach is guaranteed to find an optimal allocation for realistic task
systems running on complex target architectures. Our method is based on the
transformation of such scheduling problems into nonlinear integer
optimization problems. The core of the numerical optimization procedure we
use to discharge those problems is a solver for arbitrary Boolean
combinations of integer constraints. Optimal solutions are obtained by
imposing a binary search scheme on top of that solver. Experiments show the
applicability of our approach to industrialsize task
systems.
Subproject(s):
R2,H2

 Bibtex
 PDF restricted 
 [Swaminathan and
Fränzle, 2005]
 Mani Swaminathan and Martin Fränzle.
Automatic and scalable verification of robust realtime systems.
In Neil Jones et al., editor, Proceedings of the 17th Nordic Workshop on
Programming Theory (NWPT 05). Københavns Universitet, October 2005.
Subproject(s): H1

 Bibtex
 PDF restricted 
 [Becker et al.,
2004]
 Bernd Becker, Markus Behle, Fritz Eisenbrand, Martin
Fränzle, Marc Herbstritt, Christian Herde, Joerg Hoffmann, Daniel
Kröning, Bernhard Nebel, Ilia Polian, and Ralf Wimmer.
Bounded model checking and inductive verification of hybrid
discretecontinuous systems.
In ITG/GI/GMMWorkshop ``Methoden und Beschreibungssprachen zur
Modellierung und Verifikation von Schaltungen und Systemen'', 2004.
Abstract (click to open/close) We present a concept to significantly
advance the state of the art for bounded model checking (BMC) and inductive
verification (IV) of hybrid discretecontinuous systems. Our approach
combines the expertise of partners coming from different domains, like hybrid
systems modeling and digital circuit verification, bounded planning and
heuristic search, combinatorial optimization and integer programming. After
sketching the overall verification flow we present first results indicating
that the combination and tight integration of different verification engines
is a first step to pave the way to fully automated BMC and IV of medium to
largescale networks of hybrid
automata.
Keywords: Hybrid System Verification,
Bounded Model Checking, Inductive Verification, Verification
Engines Subproject(s): H2

 Bibtex
 PDF restricted 
 [Fränzle,
2004]
 Martin Fränzle.
Modelchecking densetime duration calculus.
Formal Aspects of Computing Science, 16(2):121139, 2004.
Subproject(s): H1

 Bibtex
 PDF restricted 
 [Fränzle and
Hansen, 2004]
 Martin Fränzle and Michael R. Hansen.
A robust interpretation of duration calculus.
In Paul Pettersson and Wang Yi, editors, Proceedings of the 16th Nordic
Workshop on Programming Theory (NWPT 04),, pages 8385. Dept. of
Information Technology, Uppsala University, 2004.
Subproject(s): H1

 Bibtex
 PDF restricted 
 [Fränzle and Herde,
2004]
 Martin Fränzle and Christian Herde.
Efficient proof engines for bounded model checking of hybrid systems.
In Ninth International Workshop on Formal Methods for Industrial Critical
Systems (FMICS 04), Electronic Notes in Theoretical Computer Science
(ENTCS). Elsevier, 2004.
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 DPLLbased pseudoBoolean 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, infinitestate systems, decision procedures,
satisfiability Subproject(s): H2

 Bibtex
 PostScript restricted 
PDF restricted 
