[24]
Model Checking and Synthesis for Branching Multi-Weighted LogicsbyJ.S. JensenI. KaufmannK.G. LarsenS.M. NielsenJ. SrbaJournal of Logical and Algebraic Methods in Programmingpages 1--30Elsevier Science2019 To appear.PDFElsevier ScienceEEBibTexAbstractWe investigate the open synthesis problem in a quantitative game theoretic setting where the system model is annotated with
multiple nonnegative weights representing quantitative resources such as energy, discrete time or cost. We consider system
specifications expressed in the branching time logic CTL extended with bounds on resources. As our first contribution, we
show that the model checking problem for the full logic is undecidable with already three weights. By restricting the bounds
to constant upper or lower-bounds on the individual weights, we demonstrate that the problem becomes decidable and that the
model checking problem is PSPACE-complete. As a second contribution, we show that by imposing upper-bounds on the temporal
operators and assuming that the cost converges over infinite runs, the synthesis problem is also decidable. Finally, we provide
an on-the-fly algorithm for the synthesis problem on an unrestricted model for a reachability fragment of the logic and we
prove EXPTIME-completeness of the synthesis problem.
[23]
Stubborn Versus Structural Reductions for Petri NetsbyF. BønnelandJ. DyhrP.G. JensenM. JohannsenJ. SrbaJournal of Logical and Algebraic Methods in Programming
volume 1021ofpages 46--63Elsevier Science2019PDFElsevier ScienceEEBibTexAbstractPartial order and structural reduction techniques are some of the most beneficial methods for state space reduction in reachability
analysis of Petri nets. This is among others documented by the fact that these techniques are used by the leading tools in
the annual Model Checking Contest (MCC) of Petri net tools. We suggest improved versions of a partial order reduction based
on stubborn sets and of a structural reduction with additional new reduction rules, and we extend both methods for the application
on Petri nets with weighted arcs and weighted inhibitor arcs. All algorithms are implemented in the open-source verification
tool TAPAAL and evaluated on a large benchmark of Petri net models from MCC'17, including a comparison with the tool LoLA
(the last year winner of the competition). The experiments document that both methods provide significant state space reductions
and, even more importantly, that their combination is indeed beneficial as a further nontrivial state space reduction can
be achieved.
[22]
MCC'2017 - The Seventh Model Checking ContestbyF. KordonH. GaravelL.-M. HillahE. Paviot-AdetL. JezequelF. Hulin-HubardE.G. AmparoreM. BeccutiB. BerthomieuH. EvrardP.G. JensenD. Le BotlanT. LiebkeJ. MeijerJ. SrbaY. Thierry-MiegJ. van de PolK. WolfT. Petri Nets and Other Models of Concurrency
volume 13ofpages 181--209Springer-Verlag2018PDFSpringer-VerlagEEBibTexAbstractCreated in 2011, the Model Checking Contest (MCC) is an annualcompetition dedicated to provide a fair evaluation of software
tools thatverify concurrent systems using state-space exploration techniques andmodel checking. This article presents the
principles and results of the2017 edition of the MCC, which took place along with the Petri Net andACSD joint conferences
in Zaragoza, Spain.
[21]
A Distributed Fixed-Point Algorithm for Extended Dependency GraphsbyA.E. DalsgaardS. EnevoldsenP. FoghL.S. JensenP.G. JensenT.S. JepsenI. KaufmannK.G. LarsenS.M. NielsenM.Chr. OlesenS. PastvaJ. SrbaFundamenta Informaticae
volume 1614ofpages 351--381IOS Press2018PDFIOS PressEEBibTexAbstractEquivalence and model checking problems can be encoded into computing fixed points on dependency graphs. Dependency graphs
represent causal dependencies among the nodes of the graph by means of hyper-edges. We suggest to extend the model of dependency
graphs with so-called negation edges in order to increase their applicability. The graphs (as well as the verification problems)
suffer from the state space explosion problem. To combat this issue, we design an on-the-fly algorithm for efficiently computing
fixed points on extended dependency graphs. Our algorithm supplements previous approaches with the possibility to back-propagate,
in certain scenarios, the domain value 0, in addition to the standard back-propagation of the value 1. Finally, we design
a distributed version of the algorithm, implement it in our open-source tool TAPAAL, and demonstrate the efficiency of our
general approach on the benchmark of Petri net models and CTL queries from the annual Model Checking Contest.
[20]
Discrete and Continuous Strategies for Timed-Arc Petri Net GamesbyP.G. JensenK.G. LarsenJ. SrbaInternational Journal on Software Tools for Technology Transfer (STTT)
volume 205ofpages 529--546Springer-Verlag2018PDFSpringer-VerlagEEBibTexAbstractAutomatic strategy synthesis for a given control objective can be used to generate correct-by-construction controllers of
real-time reactive systems. The existing symbolic approach for continuous timed games is a computationally hard task and current
tools like UPPAAL TiGa often scale poorly with the model complexity. We suggest an explicit approach for strategy synthesis
in the discrete-time setting and show that even for systems with closed guards, the existence of a safety discrete-time strategy
does not imply the existence of a safety continuous-time strategy and vice versa. Nevertheless, we prove that the answers
to the existence of discrete-time and continuous-time safety strategies coincide on a practically motivated subclass of urgent
controllers that either react immediately after receiving an environmental input or wait with the decision until a next event
is triggered by the environment. We then develop an on-the-fly synthesis algorithm for discrete timed-arc Petri net games.
The algorithm is implemented in our tool TAPAAL and based on the experimental evidence, we discuss the advantages of our approach
compared to the symbolic continuous-time techniques.
[19]
TAPAAL and Reachability Analysis of P/T NetsbyJ.F. JensenT. NielsenL.K. OestergaardJ. SrbaLNCS Transactions on Petri Nets and Other Models of Concurrency (ToPNoC)
volume 9930ofpages 307--318Springer-Verlag2016PDFSpringer-VerlagEEBibTexAbstractWe discuss selected model checking techniques used in the tool TAPAAL for the reachability analysis of weighted Petri nets
with inhibitor arcs. We focus on techniques that had the most significant effect at the 2015 Model Checking Contest (MCC).
While the techniques are mostly well known, our contribution lies in their adaptation to the MCC reachability queries, their
efficient implementation and the evaluation of their performance on a large variety of nets from MCC'15.
[18]
Efficient Model Checking of Weighted CTL with Upper-Bound ConstraintsbyJ.F. JensenK.G. LarsenJ. SrbaL.K. OestergaardInternational Journal on Software Tools for Technology Transfer (STTT)
volume 184ofpages 409--426Springer-Verlag2016PDFSpringer-VerlagEEBibTexAbstractWe present a symbolic extension of dependency graphs by Liuand Smolka in order to model-check weighted Kripke structures againstthe
logic CTL with upper-bound weight constraints. Our extension introducesa new type of edges into dependency graphs and lifts
the computation offixed-points from boolean domain to nonnegative integers in order to copewith the weights. We present both
global and local algorithms for thefixed-point computation on symbolic dependency graphs and argue for theadvantages of our
approach compared to the direct encoding of the modelchecking problem into dependency graphs. We implement all algorithmsin
a publicly available tool prototype and evaluate them on severalexperiments. The principal conclusion is that our local algorithm
isthe most efficient one with an order of magnitude improvement formodel checking problems with a high number of `witnesses'.
[17]
Soundness of Timed-Arc Workflow Nets in Discrete and Continuous-Time SemanticsbyJ.A. MateoJ. SrbaM.G. SørensenFundamenta Informaticae
volume 1401ofpages 89--121IOS Press2015PDFIOS PressEEBibTexAbstractAnalysis of workflow processes with quantitative aspectslike timing is of interest in numerous time-critical applications.
We suggest a workflow model based on timed-arc Petri nets and studythe foundational problems of soundness and strong (time-bounded)
soundness.We first consider the discrete-time semantics (integer delays)and explore the decidability of the soundness problemsand
show, among others, that soundness is decidable for monotonic workflow nets while reachability is undecidable.For general
timed-arc workflow nets soundness andstrong soundness become undecidable, though we can design efficientverification algorithms
for the subclass of bounded nets. We also discuss the soundness problem in the continuous-timesemantics (real-number delays)
and show that for nets withnonstrict guards (where the reachability question coincides for bothsemantics) the soundness checking
problem does not in generalfollow the approach for the discrete semantics and different zone-basedtechniques are needed for
introducing its decidability in the bounded case.Finally, we demonstrate the usability of our theory onthe case studies of
a Brake System Control Unit used in aircraft certification, the MPEG2 encoding algorithm, and a blood transfusion workflow.The
implementation of the algorithms is freely available as a part of the model checker TAPAAL (www.tapaal.net).
[16]
Refinement Checking on Parametric Modal Transition SystemsbyN. BenesJ. KretinskyK.G. LarsenM.H. MøllerS. SickertJ. SrbaActa Informatica
volume 522--3ofpages 269--297Springer-Verlag2015PDFSpringer-VerlagEEBibTexAbstractModal transition systems (MTS) is a well-studied specification formalism of reactive systems supporting a step-wise refinement
methodology. Despite its many advantages, the formalism as well as its currently known extensions are incapable of expressing
some practically needed aspects in the refinement process like exclusive, conditional and persistent choices. We introduce
a new model called parametric modal transition systems (PMTS) together with a general modal refinement notion that overcomes
many of the limitations. We investigate the computational complexity of modal and thorough refinement checking on PMTS and
its subclasses and provide a direct encoding of the modal refinement problem into quantified Boolean formulae, allowing us
to employ state-of-the-art QBF solvers for modal refinement checking. The experiments we report on show that the feasibility
of refinement checking is more influenced by the degree of nondeterminism rather than by the syntactic restrictions on the
types of formulae allowed in the description of the PMTS.
[15]
TCTL-Preserving Translations from Timed-Arc Petri Nets to Networks of Timed AutomatabyJ. BygM. JacobsenL. JacobsenK.Y. JørgensenM.H. MøllerJ. SrbaTheoretical Computer Science
volume 5375ofpages 3--28Elsevier Science2014PDFElsevier ScienceEEBibTexAbstractWe present a framework for TCTL-preserving translations between time-dependent modelling formalisms. The framework guarantees
that once the original and the translated system are in one-by-many correspondence relation (a notion of behavioural equivalence
between timed transition systems) then TCTL properties of the original system can be transformed too while preserving the
verification answers. We demonstrate the usability of the technique on two reductions from bounded timed-arc Petri nets to
networks for timed automata, providing unified proofs of the translations implemented in the verification tool TAPAAL. We
evaluate the efficiency of the approach on a number of experiments: alternating bit protocol, FischerÊ¼s protocol, Lynch-Shavit
protocol, MPEG-2 encoder, engine workshop and medical workflow. The results are encouraging and confirm the practical applicability
of the approach.
[14]
Model-Checking Web Services Business Activity ProtocolsbyA.P. Marques Jr.A.P. RavnJ. SrbaS. VighioInternational Journal on Software Tools for Technology Transfer (STTT)
volume 152ofpages 125--147Springer-Verlag2013PDFSpringer-VerlagEEBibTexAbstractWeb Services Business Activity specification definestwo coordination protocols BAwCC (Business Agreement with Coordination
Completion)and BAwPC (Business Agreement with Participant Completion)that ensure a consistent agreement on the outcome of
long-running distributedapplications. In order to verify fundamental properties of the protocolswe provide formal analyses
in the model checker UPPAAL.Our analyses are supported by a newly developed tool chain,where in the first step we translatetables
with state-transition protocol descriptionsinto an intermediate XML format, and in the second step wetranslate this format
into a network of communicating state machinesdirectly suitable for verification in UPPAAL.Our results show that the WS-BA
protocols, as described in the standardspecification, violate correct operation by reaching invalid statesfor all underlying
communication media except for a perfect FIFO.Hence we propose changes to the protocols and a furtherinvestigation of the
modified protocols suggests that in case ofthe BAwCC protocol messages shouldbe received in the same order as they are sent
to preserve correct behaviour,while BAwPC is now correct even for asynchronous,unordered, lossy and duplicating media.Another
important property of communication protocolsis that all parties always reach, under certain fairness assumptions,their final
states. Based on an automatic verification with differentcommunication models, we prove that our enhanced protocols satisfy
thisproperty whereas the original protocols do not.All verification results presented in this article were performedin a fully
automatic way using our new tool csv2uppaal.
[13]
EXPTIME-Completeness of Thorough Refinement on Modal Transition SystemsbyN. BenesJ. KretinskyK.G. LarsenJ. SrbaInformation and Computation
volume 218ofpages 54--68Elsevier Science2012PDFElsevier ScienceEEBibTexAbstractModal transition systems (MTS), a specification formalism introduced more than 20 years ago, has recently received a considerable
attention in several different areas. Many of the fundamental questions related to MTSs have already been answered. However,
the problem of the exact computational complexity of thorough refinement checking between two finite MTSs remained unsolved.
We settle down this question by showing EXPTIME-completeness of thorough refinement checking on finite MTSs. The upper-bound
result relies on a novel algorithm running in single exponential time providing a direct goal-oriented way to decide thorough
refinement. If the right-hand side MTS is moreover deterministic, or has a fixed size, the running time of the algorithm becomes
polynomial. The lower-bound proof is achieved by reduction from the acceptance problem of alternating linear bounded automata
and the problem remains EXPTIME-hard even if the left-hand side MTS is fixed and deterministic.
[12]
Extending Modal Transition Systems with Structured LabelsbyS.S. BauerL. JuhlK.G. LarsenA. LegayJ. SrbaMathematical Structures in Computer Science
volume 224ofpages 581--617Cambridge University Press2012PDFCambridge University PressEEBibTexAbstractWe introduce a novel formalism of label-structured modal transition systems that combines the classical may/must modalities
on transitions with structured labels that represent quantitative aspects of the model. On the one hand, the specification
formalism is general enough to include models like weighted modal transition systems and allows the system developers to employ
more complex label refinement than in the previously studied theories. On the other hand, the formalism maintains the desirable
properties required by any specification theory supporting compositional reasoning. In particular, we study modal and thorough
refinement, determinization, parallel composition, conjunction, quotient, and logical characterization of label-structured
modal transition systems.
[11]
Modal Transition Systems with Weight IntervalsbyL. JuhlK.G. LarsenJ. SrbaJournal of Logic and Algebraic Programming
volume 814ofpages 408--421Elsevier Science2012PDFElsevier ScienceBibTexAbstractWe propose weighted modal transition systems, an extension to the well-studied specification formalism of modal transition
systems that allows to express both required and optional behaviours of their intended implementations. In our extension we
decorate each transition with a weight interval that indicates the range of concrete weight values available to the potential
implementations. In this way resource constraints can be modelled using the modal approach. We focus on two problems. First,
we study the question of existence/finding the largest common refinement for a number of finite deterministic specifications
and we show PSPACE-completeness of this problem. By constructing the most general common refinement, we allow for a stepwise
and iterative construction of a common implementation. Second, we study a logical characterisation of the formalism and show
that a formula in a natural weight extension of the logic CTL is satisfied by a given modal specification if and only if it
is satisfied by all its refinements. The weight extension is general enough to express different sorts of properties that
we want our weights to satisfy.
[10]
On Determinism in Modal Transition SystemsbyN. BenesJ. KretinskyK.G. LarsenJ. SrbaTheoretical Computer Science
volume 41041ofpages 4026--4043Elsevier Science2009PDFElsevier ScienceEEBibTexAbstractModal transition system (MTS) is a formalism which extends the classical notion of labelled transition systems by introducing
transitions of two types: must transitions that have to be present in any implementation of the MTS and may transitions that
are allowed but not required. The MTS framework has proved to be useful as a specification formalism of component-based systems
as it supports compositional verification and stepwise refinement. Nevertheless, there are some limitations of the theory,
namely that the naturally defined notions of modal refinement and modal composition are incomplete with respect to the semantic
view based on the sets of the implementations of a given MTS specification. Recent work indicates that some of these limitations
might be overcome by considering deterministic systems, which seem to be more manageable but still interesting for several
application areas. In the present article, we provide a comprehensive account of the MTS framework in the deterministic setting.
We study a number of problems previously considered on MTS and point out to what extend we can expect better results under
the restriction of determinism.
[9]
Beyond Language Equivalence on Visibly Pushdown AutomatabyJ. SrbaLogical Methods in Computer Science
volume 51:2ofpages 1--22Creative Commons2009PDFCreative CommonsEEBibTexAbstractWe study (bi)simulation-like preorder/equivalence checking on the class of visibly pushdown automata and its natural subclasses
visibly BPA (Basic Process Algebra) and visibly one-counter automata. We describe generic methods for proving complexity upper
and lower bounds for a number of studied preorders and equivalences like simulation, completed simulation, ready simulation,
2-nested simulation preorders/equivalences and bisimulation equivalence. Our main results are that all the mentioned equivalences
and preorders are EXPTIME-complete on visibly pushdown automata, PSPACE-complete on visibly one-counter automata and P-complete
on visibly BPA. Our PSPACE lower bound for visibly one-counter automata improves also the previously known DP-hardness results
for ordinary one-counter automata and one-counter nets. Finally, we study regularity checking problems for visibly pushdown
automata and show that they can be decided in polynomial time.
[8]
Undecidability of Bisimilarity by Defender's ForcingbyP. JancarJ. SrbaJournal of the ACM
volume 551ofpages 1--26ACM2008PDFACMEEBibTexAbstractStirling (1996, 1998) proved the decidability of bisimilarity on so-called normed pushdown processes. This result was substantially
extended by Senizergues(1998, 2005) who showed the decidability of bisimilarity for regular (or equational) graphs of finite
out-degree; this essentially coincides with weak bisimilarity of processes generated by (unnormed) pushdown automata where
the epsilon-transitions can only deterministically pop the stack. The question of decidability of bisimilarity for the more
general class of so called Type -1 systems, which is equivalent to weak bisimilarity on unrestricted epsilon-popping pushdown
processes, was left open. This was repeatedly indicated by both Stirling and Senizergues. Here we answer the question negatively,
that is, we show the undecidability of bisimilarity on Type -1 systems, even in the normed case. We achieve the result by
applying a technique we call Defender's Forcing, referring to the bisimulation games. The idea is simple, yet powerful. We
demonstrate its versatility by deriving further results in a uniform way. First, we classify several versions of the undecidable
problems for prefix rewrite systems (or pushdown automata) as Pi^0_1-complete or Sigma^1_1-complete. Second, we solve the
decidability question for weak bisimilarity on PA (Process Algebra) processes, showing that the problem is undecidable and
even Sigma^1_1-complete. Third, we show Sigma^1_1-completeness of weak bisimilarity for so-called parallel pushdown (or multiset)
automata, a subclass of (labeled, place/transition) Petri nets.
[7]
Decidability Issues for Extended Ping-Pong ProtocolsbyH. HüttelJ. SrbaJournal of Automated Reasoning
volume 361--2ofpages 125--147Kluwer2006PDFKluwerEEBibTexAbstractWe use some recent techniques from process algebra to draw several conclusions about the well studied class of ping-pong protocols
introduced by Dolev and Yao. In particular we show that all nontrivial properties, including reachability and equivalence
checking wrt. the whole van Glabbeek's spectrum, become undecidable for a very simple recursive extension of the protocol.
The result holds even if no nondeterministic choice operator is allowed but reachability is shown to be decidable in polynomial
time if only two parties are participating in the protocol. We also show that the calculus is capable of an implicit description
of the active intruder, including full analysis and synthesis of messages in the sense of Amadio, Lugiez and Vanackere. We
conclude by showing that reachability analysis for a replicative variant of the protocol becomes decidable.
[6]
On the Computational Complexity of Bisimulation, ReduxbyF. MollerS.A. SmolkaJ. SrbaInformation and Computation
volume 1922ofpages 129--143Elsevier Science2004PDFElsevier ScienceEEBibTexAbstractParis Kanellakis and the second author (Smolka) were among the first to investigate the computational complexity of bisimulation,
and the first and third authors (Moller and Srba) have long-established track records in the field. Smolka and Moller have
also written a brief survey about the computational complexity of bisimulation [Moller,Smolka'95]. The authors believe that
the special issue of Information and Computation devoted to PCK50: Principles of Computing and Knowledge: Paris C. Kanellakis
Memorial Workshop represents an ideal opportunity for an up-to-date look at the subject.
[5]
Roadmap of Infinite ResultsbyJ. SrbaBulletin of the European Association for Theoretical Computer Science, Columns: Concurrency
volume 78ofpages 163--1752002EEBibTexAbstractThis paper provides a comprehensive summary of equivalence checking results for infinite-state systems. References to the
relevant papers will be updated continuously according to the development in the area. The most recent version of this document
is available from the EE web-page.
[4]
Strong Bisimilarity of Simple Process Algebras: Complexity Lower BoundsbyJ. SrbaActa Informatica
volume 39ofpages 469--499Springer-Verlag2003PDFSpringer-VerlagEEBibTexAbstractWe study bisimilarity and regularity problems of simple process algebras. In particular, we show PSPACE-hardness of the following
problems: (i) strong bisimilarity of Basic Parallel Processes (BPP), (ii) strong bisimilarity of Basic Process Algebra (BPA),
(iii) strong regularity of BPP, and (iv) strong regularity of BPA. We also demonstrate NL-hardness of strong regularity problems
for the normed subclasses of BPP and BPA. Bisimilarity problems of simple process algebras are introduced in a general framework
of process rewrite systems, and a uniform description of the new techniques used for the hardness proofs is provided.
[3]
Undecidability of Domino Games and Hhp-BisimilaritybyM. JurdzinskiM. NielsenJ. SrbaInformation and Computation
volume 1842ofpages 343--368Elsevier Science2003PDFElsevier ScienceEEBibTexAbstract History preserving bisimilarity (hp-bisimilarity) and hereditary history preserving bisimilarity (hhp-bisimilarity) are behavioural
equivalences taking into account causal relationships between events of concurrent systems. Their prominent feature is that
they are preserved under action refinement, an operation important for the top-down design of concurrent systems. It is shown
that, in contrast to hp-bisimilarity, checking hhp-bisimilarity for finite labelled asyn\-chro\-nous transition systems is
undecidable, by a reduction from the halting problem of 2-counter machines. To make the proof more transparent a novel intermediate
problem of checking domino bisimilarity for origin constrained tiling systems is introduced and shown undecidable. It is also
shown that the unlabelled domino bisimilarity problem is undecidable, which implies undecidability of hhp-bisimilarity for
unlabelled finite asynchronous systems. Moreover, it is argued that the undecidability of hhp-bisimilarity holds for finite
elementary net systems and 1-safe Petri nets.
[2]
Complexity of Weak Bisimilarity and Regularity for BPA and BPPbyJ. SrbaMathematical Structures in Computer Science
volume 13ofpages 567--587Cambridge University Press2003PDFCambridge University PressEEBibTexAbstractIt is an open problem whether weak bisimilarity is decidable for Basic Process Algebra (BPA) and Basic Parallel Processes
(BPP). A PSPACE lower bound for BPA and NP lower bound for BPP were demonstrated by Stribrna. Mayr recently achieved a result,
saying that weak bisimilarity for BPP is a hard problem for the second level of polynomial hierarchy. We improve this lower
bound to PSPACE, moreover for the restricted class of normed BPP. Weak regularity (finiteness) of BPA and BPP is not known
to be decidable either. In the case of BPP there is a hardness result for the second level of arithmetical hierarchy by Mayr,
which we improve to PSPACE. No lower bound has previously been established for BPA. We demonstrate DP-hardness, which in particular
implies both NP and coNP-hardness. In each of the bisimulation/regularity problems we consider also the classes of normed
processes. Finally we show how the technique for proving co-NP lower bound for weak bisimilarity of BPA can be applied to
strong bisimilarity of BPP.
[1]
Basic Process Algebra with Deadlocking StatesbyJ. SrbaTheoretical Computer Science
volume 2661--2ofpages 605--630Elsevier Science2001PDFElsevier ScienceEEBibTexAbstractBisimilarity and regularity are decidable properties for the class of BPA (or context--free) processes. We extend BPA with
a deadlocking state obtaining BPAd systems. We show that the BPAd class is more expressive w.r.t. bisimilarity, but it remains
language equivalent to BPA. We prove that bisimilarity and regularity remain decidable for BPAd. Finally we give a characterisation
of those BPAd processes that can be equivalently (up to bisimilarity) described within the pure BPA syntax.