Ergebnisse der Suche:
 [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)
 [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 
 [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 
 [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 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,
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)
 [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)
 [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
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.,
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 
 [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)
 [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)
 [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 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 
