TAPAAL and Reachability Analysis of P/T NetsLNCS Transactions on Petri Nets and Other Models of Concurrency (ToPNoC)pages 1--12Springer-Verlag2016 To appear.PDFSpringer-VerlagBibTexAbstract
We 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.
Soundness of Timed-Arc Workflow Nets in Discrete and Continuous-Time SemanticsFundamenta Informaticae
volume 1401ofpages 89--121IOS Press2015PDFIOS PressEEBibTexAbstract
Analysis 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).
Refinement Checking on Parametric Modal Transition SystemsActa Informatica
volume 522--3ofpages 269--297Springer-Verlag2015PDFSpringer-VerlagEEBibTexAbstract
Modal 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.
Efficient Model Checking of Weighted CTL with Upper-Bound ConstraintsInternational Journal on Software Tools for Technology Transfer (STTT)pages 1--18Springer-Verlag2014PDFSpringer-VerlagEEBibTexAbstract
We 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'.
TCTL-Preserving Translations from Timed-Arc Petri Nets to Networks of Timed AutomataTheoretical Computer Science
volume 5375ofpages 3--28Elsevier Science2014PDFElsevier ScienceEEBibTexAbstract
We 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.
Model-Checking Web Services Business Activity ProtocolsInternational Journal on Software Tools for Technology Transfer (STTT)
volume 152ofpages 125--147Springer-Verlag2013PDFSpringer-VerlagEEBibTexAbstract
Web 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.
EXPTIME-Completeness of Thorough Refinement on Modal Transition SystemsInformation and Computation
volume 218ofpages 54--68Elsevier Science2012PDFElsevier ScienceEEBibTexAbstract
Modal 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.
Extending Modal Transition Systems with Structured LabelsMathematical Structures in Computer Science
volume 224ofpages 581--617Cambridge University Press2012PDFCambridge University PressEEBibTexAbstract
We 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.
Modal Transition Systems with Weight IntervalsJournal of Logic and Algebraic Programming
volume 814ofpages 408--421Elsevier Science2012PDFElsevier ScienceBibTexAbstract
We 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.
On Determinism in Modal Transition SystemsTheoretical Computer Science
volume 41041ofpages 4026--4043Elsevier Science2009PDFElsevier ScienceEEBibTexAbstract
Modal 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.
Beyond Language Equivalence on Visibly Pushdown AutomataLogical Methods in Computer Science
volume 51:2ofpages 1--22Creative Commons2009PDFCreative CommonsEEBibTexAbstract
We 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.
Undecidability of Bisimilarity by Defender's ForcingJournal of the ACM
volume 551ofpages 1--26ACM2008PDFACMEEBibTexAbstract
Stirling (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.
Decidability Issues for Extended Ping-Pong ProtocolsJournal of Automated Reasoning
volume 361--2ofpages 125--147Kluwer2006PDFKluwerEEBibTexAbstract
We 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.
On the Computational Complexity of Bisimulation, ReduxInformation and Computation
volume 1922ofpages 129--143Elsevier Science2004PDFElsevier ScienceEEBibTexAbstract
Paris 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.
Roadmap of Infinite ResultsBulletin of the European Association for Theoretical Computer Science, Columns: Concurrency
volume 78ofpages 163--1752002EEBibTexAbstract
This 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.
Strong Bisimilarity of Simple Process Algebras: Complexity Lower BoundsActa Informatica
volume 39ofpages 469--499Springer-Verlag2003PDFSpringer-VerlagEEBibTexAbstract
We 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.
Undecidability of Domino Games and Hhp-BisimilarityInformation 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.
Complexity of Weak Bisimilarity and Regularity for BPA and BPPMathematical Structures in Computer Science
volume 13ofpages 567--587Cambridge University Press2003PDFCambridge University PressEEBibTexAbstract
It 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.
Basic Process Algebra with Deadlocking StatesTheoretical Computer Science
volume 2661--2ofpages 605--630Elsevier Science2001PDFElsevier ScienceEEBibTexAbstract
Bisimilarity 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.