Ergebnisse der Suche:
- [Fränzle et al.,
2015]
- Martin Fränzle, Sebastian Gerwinn, Paul Kröger,
Alessandro Abate, and Joost-Pieter Katoen.
Multi-objective 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 93-107. 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 discrete-continuous 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 multi-objective 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
295-311. 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 traffic-hazard 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, state-exploratory
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 interval-based Taylor overapproximations
of the time-wise 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)
- [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 203-215. Springer
International Publishing Switzerland, 2014.
Abstract (click to open/close) Craig interpolation is widely used in
solving reachability and model-checking 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 non-polynomial 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 SSMT-based model-checking 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 assumption-commitment
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
transformation-based compositional verification approach for verifying
assumption-commitment 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 semi-hierarchical
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 semi-hierarchically structured ---, thus
expanding the frontier from decomposing purely hierarchically structured
systems to decomposing semi-hierarchically 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 |
- [Eggers et al.,
2012b]
- Andreas Eggers, Nacim Ramdani, Nedialko S. Nedialkov,
and Martin Fränzle.
Set-membership estimation of hybrid systems via SAT modulo ODE.
In Michel Kinnaert, editor, Proceedings of the 16th IFAC Symposium on
System Identification, pages 440-445. 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 integer-valued variables have made significant
progress, as they can effectively deal with algebraic constraints between
variables and non-linear 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
self-stabilizing 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 |
- [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 172-187. 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
VNODE-LP, as a state-of-the-art enclosure method for ODEs, and with
bracketing systems which--by exploiting monotonicity properties of the
system--allow finding enclosures for problems that VNODE-LP alone cannot
enclose tightly. We apply our method to the analysis of a non-linear 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 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 43-52, 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 continuous-time
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
non-determinism 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 non-linear 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 computer-aided
verification rely heavily on constraint solvers. The correctness and
reliability of these solvers are of vital importance in the analysis of
safety-critical 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 non-linear 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, 21-23 September, 2011. Proceedings, Lecture Notes in Computer
Science (LNCS). Springer-Verlag, 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,
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 158-172. 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 SSAT-based 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)
- [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 168-182. 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., mean-times 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 (LPAR-17), volume 6397 of Logic for Programming,
Artificial Intelligence, and Reasoning, pages 625-639.
Springer-Verlag, 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 PSPACE-complete 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)
- [Eggers et al., 2009a]
- Andreas Eggers, Martin
Fränzle, and Christian Herde.
Application of constraint solving and ode-enclosure 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
1326-1330, 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 discrete-continuous systems by reduction to
constraint solving paired with enclosure methods for sets of initial value
problems of ordinary differential
equations.
Keywords: hybrid discrete-continuous
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
Swaminathan, 2009]
- Martin Fränzle and Mani Swaminathan.
Revisiting decidability and optimum reachability for multi-priced 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 149-163. Springer, September 2009.
Abstract (click to open/close) We investigate the optimum
reachability problem for Multi-Priced 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 Multi-Priced 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 quasi-cyclic 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 discrete-continuous systems.
In Modern Computational Science 09, pages 363-378. BIS-Verlag 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 26-28, 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 non-linear 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 27-36.
Universitätsverlag TU Berlin, 2009.
Abstract (click to open/close) Symbolic methods in computer-aided
verification rely on appropriate constraint solvers. Correctness and
reliability of solvers are a vital requirement in the analysis of
safety-critical 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
non-linear arithmetic constraint formulae. Such formulae arise in the
analysis of hybrid discrete-continuous
systems.
Subproject(s):
H1/2
|
|  Bibtex
|  PDF restricted |
- [Teige and Fränzle,
2009]
- Tino Teige and Martin Fränzle.
Constraint-based 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 162-167.
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 scheduled-event 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.,
2008c]
- Andreas Eggers, Martin Fränzle, and Christian Herde.
SAT modulo ODE: A direct SAT approach to hybrid systems.
In Sungdeok (Steve) Cha, Jin-Young 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
171-185. Springer-Verlag, 2008.
Abstract (click to open/close) In order to facilitate automated
reasoning about large Boolean combinations of non-linear arithmetic
constraints involving ordinary differential equations (ODEs), we provide a
seamless integration of safe numeric overapproximation of initial-value
problems into a SAT-modulo-theory (SMT) approach to interval-based arithmetic
constraint solving. Interval-based safe numeric approximation of ODEs is used
as an interval contractor being able to narrow candidate sets in phase space
in both temporal directions: post-images 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, pre-images are narrowed
based on partial knowledge about post-sets. 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
interval-based 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
436-466. 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 branching-time
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 63-72. Institute of Electrical and Electronics Engineers (IEEE)
Computer Society Press, 2008.
Abstract (click to open/close) Duration Calculus (abbreviated to DC)
is an intervalbased, 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. We here
investigate a similar approximation as frequently employed in model checking
situation-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 origin of a set of linear traces, we define a branching-time counterpart
to intervalbased temporal logics building on situation pairs spanning sets of
intervals. While this branching-time interval semantics yields the desired
reduction in complexity of the modelchecking problem, from non-elementary 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.
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 172-186. 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 satisfiability-modulotheory 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 SMT-based bounded model-checking 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 finite-state
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, Pre-Proceedings 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 172-186. Springer-Verlag, 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 satisfiability-modulo-theory solving (SMT) by a comprehensive
treatment of randomized (a.k.a. stochastic) quantification over discrete
variables within the mixed Boolean-arithmetic constraint system. This
provides the technological basis for a fully symbolic analysis of
probabilistic hybrid automata. Generalizing SMT-based bounded model-checking
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 finite-state 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 196-201. 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 safety-critical
embedded systems with HySAT. HySAT is an arithmetic constraint solver with a
tightly integrated bounded model checker for hybrid discrete-continuous
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 |
- [Swaminathan
et al., 2008]
- Mani Swaminathan, Martin Fränzle, and
Joost-Pieter Katoen.
The surprising robustness of (closed) timed automata against
clock-drift.
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 537-553. Springer-Verlag, 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 two-fold: (1) We first consider the
model of clock-drift introduced by Puri [1] and subsequently studied in other
works [2,3,4]. We show that the standard zone-based 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 clock-drift, for TA with closed guards,
invariants, and targets, but now without any restrictions on system
life-time.
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 non-linear 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 248-262.
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
non-linear 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 non-linear
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)
- [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 201-215. Springer, 2007.
Abstract (click to open/close) A decidability result and a
model-checking procedure for a rich subset of Duration Calculus (DC) [19] is
obtained through reductions to is obtained through reductions to First-order
logic over the real-closed field and to Multi-Priced 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: Real-time systems, metric-time
temporal logic, decidability, model-checking, multi-priced timed
automata Subproject(s): H1
|
|  Bibtex
|  PDF restricted |
© Springer Verlag (see article at SpringerLink)
- [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 clock-drift. 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 region-based (Puri, 2000), (DeWulf, Doyen, Markey,
and Raskin, 2004), or involve a combination of forward and backward analyses
when zone-based (Daws and Kordy, 2006), ours is a zone-based 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 two-watched-literal scheme in a mixed boolean and non-linear
arithmetic constraint solver.
In José Neves, Manuel Filipe Santos, and José Manuel Machado, editors,
Proceedings of the 13th Portuguese Conference on Artificial
Intelligence (EPIA 2007), New Trends in Artificial Intelligence, pages
729-741. APPIA, December 2007.
Abstract (click to open/close) In its combination with
conflict-driven clause learning the two-watched-literal 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 two-watched-atom scheme,
implemented in our interval-based constraint solver HySAT, the latter being a
solver for mixed Boolean and non-linear 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 speed-up 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
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.
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 14-21, 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 real-valued, potentially time-continuous,
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 pre-planned 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 forward-backward interval constraint propagation. On both
layers learning algorithms are applied in order to avoid the spending of
computation time on paths and sub-constraints, 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 81-95, 2006.
Abstract (click to open/close) In order to facilitate automated
reasoning about large Boolean combinations of non-linear arithmetic
constraints involving transcendental functions, we extend the paradigm of
lazy theorem proving to interval-based 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 interval-based constraint solving with all the algorithmic
enhancements that were instrumental to the enormous performance gains
recently achieved in propositional SAT solving, like conflict-driven learning
combined with non-chronological
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 SAT-based approach to
the task and message allocation problem of distributed real-time 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 industrial-size
task systems, which are mapped to heterogeneous hierarchical hardware
architectures.
Subproject(s):
R2,H2
|
|  Bibtex
|  PDF restricted |
- [Enslev et
al., 2005]
- Jacob Enslev, Anne-Sofie 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
257-271. Springer Verlag, 2005.
Abstract (click to open/close) We transfer the concept of robust
interpretation from arithmetic first-order theories to metric-time 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 multi-valued
interpretation that uses the real numbers as semantic domain and assigns
Lipschitz-continuous interpretations to all operators of DC. Furthermore,
this continuity permits approximation between discrete and dense time, thus
allowing exploitation of discrete-time (semi-)decision procedures on
dense-time properties.
Keywords: Metric-time
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 Real-Time Systems by Satisfiability Checking.
In Proceedings of the IEEE Conference on Embedded and Real-Time Computing
Systems and Applications, pages 409-415. IEEE Computer Society, 2005.
Abstract (click to open/close) We present a SAT-based approach to
the task and message allocation problem of distributed real-time 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 industrial-size 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 real-time 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
discrete-continuous systems.
In ITG/GI/GMM-Workshop ``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 discrete-continuous 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
large-scale networks of hybrid
automata.
Keywords: Hybrid System Verification,
Bounded Model Checking, Inductive Verification, Verification
Engines Subproject(s): H2
|
|  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 83-85. 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 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 |
|