[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.
