@inproceedings{DFLSZZ:CBSE:12,
author ={R. Dong and J. Faber and Zh. Liu and J. Srba and N. Zhan and J. Zhu},
title ={Unblockable Compositions of Software Components},
booktitle ={Proceedings of the 15th International ACM SIGSOFT Symposium on Component Based Software Engineering ({CBSE}'12)},
year ={2012},
publisher ={ACM},
abstract ={We present a new automata-based interface model describing the interaction behavior of software components. Contrary to earlier component- or interface-based approaches, the interface model we propose specifies all the non-blockable interaction behaviors of a component with any environment. To this end, we develop an algorithm to compute the unblockable interaction behavior, called the interface model of a component, from its execution model. Based on this model, we introduce composition operators for the components and prove important compositionality results, showing the conditions under which composition of interface models preserves unblockable sequences of provided services.},
note ={To appear.},
pdf ={http://www.brics.dk/~srba/files/DFLSZZ:CBSE:12.pdf},
}

@inproceedings{BJLLS:TASE:12,
author ={S.S. Bauer and L. Juhl and K.G. Larsen and A. Legay and J. Srba},
title ={A Logic for Accumulated-Weight Reasoning on Multiweighted Modal Automata},
booktitle ={Proceedings of the 6th International Symposium on Theoretical Aspects of Software Engineering ({TASE}'12)},
year ={2012},
publisher ={IEEE Computer Society Press},
abstract ={Multiweighted modal automata provide a specification theory for multiweighted transition systems that have recently attracted interest in the context of energy games. We propose a simple fragment of CTL that is able to express properties about accumulated weights along maximal runs of multiweighted modal automata. Our logic is equipped with a game-based semantics and guarantees both soundness (formula satisfaction is propagated to the modal refinements) as well as completeness (formula non-satisfaction is propagated to at least one of its implementations). We augment our theory with a summary of decidability and complexity results of the generalized model checking problem, asking whether a specification---abstracting the whole set of its implementations---satisfies a given formula.},
note ={To appear.},
pdf ={http://www.brics.dk/~srba/files/BJLLS:TASE:12.pdf},
}

@inproceedings{BKLMS:LPAR:12,
author ={N. Bene\v{s} and J. K\v{r}et\'{\i}nsk\'{y} and K.G. Larsen and M.H. M{\o}ller and J. Srba},
title ={Dual-Priced Modal Transition Systems with Time Durations},
booktitle ={Proceedings of the 18th International Conference on Logic for Programming, Artificial Intelligence and Reasoning ({LPAR}'12)},
year ={2012},
series ={LNCS},
volume ={7180},
publisher ={Springer-Verlag},
pages ={122--137},
abstract ={Modal transition systems are a well-established specification formalism for a high-level modelling of component-based software systems. We present a novel extension of the formalism called modal transition systems with durations where time durations are modelled as controllable or uncontrollable intervals. We further equip the model with two kinds of quantitative aspects: each action has its own running cost per time unit, and actions may require several hardware components of different costs. We ask the question, given a fixed budget for the hardware components, what is the implementation with the cheapest long-run average reward. We give an algorithm for computing such optimal implementations via a reduction to a new extension of mean payoff games with time durations and analyse the complexity of the algorithm.},
pdf ={http://www.brics.dk/~srba/files/BKLMS:LPAR:12.pdf},
ee ={http://www.springerlink.com/content/2767663q35650317},
}

@inproceedings{DJJJMS:TACAS:12,
author ={A. David and L. Jacobsen and M. Jacobsen and K.Y. J{\o}rgensen and M.H. M{\o}ller and J. Srba},
title ={TAPAAL 2.0: Integrated Development Environment for Timed-Arc Petri Nets},
booktitle ={Proceedings of the 18th International Conference on Tools and Algorithms for the Construction and Analysis of Systems ({TACAS}'12)},
year ={2012},
series ={LNCS},
volume ={7214},
publisher ={Springer-Verlag},
pages ={492--497},
abstract ={TAPAAL 2.0 is a platform-independent modelling, simulation and verification tool for extended timed-arc Petri nets. The tool supports component-based modelling and offers an automated verification of the EF, AG, EG and AF fragments of TCTL via translations to Uppaal timed automata and via its own dedicated verification engine. After more than three years of active development with a main focus on usability aspects and on the efficiency of the verification algorithms, we present the new version of TAPAAL 2.0 that has by now reached its maturity and offers the first publicly available tool supporting the analysis and verification of timed-arc Petri nets.},
pdf ={http://www.brics.dk/~srba/files/DJJJMS:TACAS:12.pdf},
ee ={http://dx.doi.org/10.1007/978-3-642-28756-5_36},
}

@inproceedings{MRSV:TTSS:11,
author ={A.P. Marques Jr. and A.P. Ravn and J. Srba and S. Vighio},
title ={Tool Supported Analysis of Web Services Protocols},
booktitle ={Proceedings of the 5th International Workshop of Harnessing Theories for Tool Support in Software ({TTSS}'11)},
year ={2011},
pages ={50--64},
abstract ={We describe an abstract protocol model suitable for modelling of web services and other protocols communicating via unreliable, asynchronous communication channels. The model is supported by a tool chain where the first step translates tables with state/transition protocol descriptions, often used e.g. in the design of web services protocols, into an intermediate XML format. We further translate this format into a network of communicating state machines directly suitable for verification in the model checking tool UPPAAL. We introduce two types of communication media abstractions in order to ensure the finiteness of the protocol state-spaces while still being able to verify interesting protocol properties. The translations for different kinds of communication media have been implemented and successfully tested, among others, on agreement protocols from WS-Business Activity.},
pdf ={http://www.brics.dk/~srba/files/MRSV:TTSS:11.pdf},
ee ={http://www.duo.uio.no/sok/work.html?WORKID=137619},
}

@inproceedings{BKLMS:ATVA:11,
author ={N. Bene\v{s} and J. K\v{r}et\'{\i}nsk\'{y} and K.G. Larsen and M.H. M{\o}ller and J. Srba},
title ={Parametric Modal Transition Systems},
booktitle ={Proceedings of the 9th International Symposium on Automated Technology for Verification and Analysis ({ATVA}'11)},
year ={2011},
series ={LNCS},
volume ={6996},
publisher ={Springer-Verlag},
pages ={275--289},
abstract ={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 overcome many of the limitations and we investigate the computational complexity of modal refinement checking.},
pdf ={http://www.brics.dk/~srba/files/BKLMS:ATVA:11.pdf},
ee ={http://dx.doi.org/10.1007/978-3-642-24372-1_20},
}

@inproceedings{FJLS:ICTAC:11,
author ={U. Fahrenberg and L. Juhl and K.G. Larsen and J. Srba},
title ={Energy Games in Multiweighted Automata},
booktitle ={Proceedings of the 8th International Colloquium on Theoretical Aspects of Computing ({ICTAC}'11)},
year ={2011},
series ={LNCS},
volume ={6916},
pages ={95--115},
publisher ={Springer-Verlag},
abstract ={Energy games have recently attracted a lot of attention. These are games played on finite weighted automata and concern the existence of infinite runs subject to boundary constraints on the accumulated weight, allowing \eg~only for behaviours where a resource is always available (nonnegative accumulated weight), yet does not exceed a given maximum capacity. We extend energy games to a multiweighted and parameterized setting, allowing us to model systems with multiple quantitative aspects. We present reductions between Petri nets and multiweighted automata and among different types of multiweighted automata and identify new complexity and (un)decidability results for both one- and two-player games. We also investigate the tractability of an extension of multiweighted energy games in the setting of timed automata.},
pdf ={http://www.brics.dk/~srba/files/FJLS:ICTAC:11.pdf},
ee ={http://www.springerlink.com/content/k6513r055t55j187/},
}

@inproceedings{DHJLOOS:NFM:11,
author ={A.E. Dalsgaard and R.R. Hansen and K.Y. J{\o}rgensen and K.G. Larsen and M.Chr. Olesen and P. Olsen and J. Srba},
title ={opaal: A Lattice Model Checker},
booktitle ={Proceedings of the 3rd NASA Formal Methods Symposium ({NFM}'11)},
year ={2011},
series ={LNCS},
volume ={6617},
publisher ={Springer-Verlag},
pages ={487--493},
abstract ={We present a new open source model checker, opaal, for automatic verification of models using lattice automata. Lattice automata allow the users to incorporate abstractions of a model into the model itself. This provides an efficient verification procedure, while giving the user fine-grained control of the level of abstraction by using a method similar to Counter-Example Guided Abstraction Refinement. The opaal engine supports a subset of the UPPAAL timed automata language extended with lattice features. We report on the status of the first public release of opaal, and demonstrate how opaal can be used for efficient verification on examples from domains such as database programs, lossy communication protocols and cache analysis.},
pdf ={http://www.brics.dk/~srba/files/DHJLOOS:NFM:11.pdf},
ee ={http://www.springerlink.com/content/978-3-642-20397-8},
}

@inproceedings{RSV:TACAS:11,
author ={A.P. Ravn and J. Srba and S. Vighio},
title ={Modelling and Verification of Web Services Business Activity Protocol},
booktitle ={Proceedings of the 17th International Conference on Tools and Algorithms for the Construction and Analysis of Systems ({TACAS}'11)},
year ={2011},
series ={LNCS},
volume ={6605},
publisher ={Springer-Verlag},
pages ={357--371},
abstract ={WS-Business Activity specification defines two coordination protocols in order to ensure a consistent agreement on the outcome of long-running distributed applications. We use the model checker Uppaal to analyse the Business Agreement with Coordination Completion protocol type. Our analyses show that the protocol, as described in the standard specification, violates correct operation by reaching invalid states for all underlying communication media except for the perfect FIFO. Based on this result, we propose changes to the protocol. A further investigation of the modified protocol suggests that messages should be received in the same order as they are sent so that a correct protocol behaviour is preserved. Another important property of communication protocols is that all parties always reach their final states. Based on the verification with different communication models, we prove that our enhanced protocol satisfies this property for asynchronous, unreliable, order-preserving communication whereas the original protocol does not.},
pdf ={http://www.brics.dk/~srba/files/RSV:TACAS:11.pdf},
ee ={http://www.springerlink.com/content/jm74684627718671/},
}

@inproceedings{JJMS:SOFSEM:11,
author ={L. Jacobsen and M. Jacobsen and M.H. M{\o}ller and J. Srba},
title ={Verification of Timed-Arc {P}etri Nets},
booktitle ={Proceedings of the 37th International Conference on Current Trends in Theory and Practice of Computer Science ({SOFSEM}'11)},
year ={2011},
series ={LNCS},
volume ={6543},
publisher ={Springer-Verlag},
pages ={46--72},
abstract ={Timed-Arc Petri Nets (TAPN) are an extension of the classical P/T nets with continuous time. Tokens in TAPN carry an age and arcs between places and transitions are labelled with time intervals restricting the age of tokens available for transition firing. The TAPN model posses a number of interesting theoretical properties distinguishing them from other time extensions of Petri nets. We shall give an overview of the recent theory developed in the verification of TAPN extended with features like read/transport arcs, timed inhibitor arcs and age invariants. We will examine in detail the boundaries of automatic verification and the connections between TAPN and the model of timed automata. Finally, we will mention the tool TAPAAL that supports modelling, simulation and verification of TAPN and discuss a small case study of alternating bit protocol.},
pdf ={http://www.brics.dk/~srba/files/JJMS:SOFSEM:11.pdf},
ee ={http://www.springerlink.com/content/ek83j00501734324/},
}

@inproceedings{RVS:ISOLA:10,
author ={A.P. Ravn and J. Srba and S. Vighio},
title ={A Formal Analysis of the Web Services Atomic Transaction Protocol with UPPAAL},
booktitle ={Proceedings of the 4th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation ({ISOLA}'10)},
year ={2010},
series ={LNCS},
volume ={6416},
publisher ={Springer-Verlag},
pages ={579--593},
abstract ={We present a formal analysis of the Web Services Atomic Transaction (WS-AT) protocol. WS-AT is a part of the WS-Coordination framework and describes an algorithm for reaching agreement on the outcome of a distributed transaction. The protocol is modelled and verified using the model checker UPPAAL. Our model is based on an already available formalization using the mathematical language TLA+ where the protocol was verified using the model checker TLC. We discuss the key aspects of these two approaches, including the characteristics of the specification languages, the performances of the tools, and the robustness of the specifications with respect to extensions.},
pdf ={http://www.brics.dk/~srba/files/RVS:ISOLA:10.pdf},
ee ={http://www.springerlink.com/content/y0jk3h2127567401/},
}

@inproceedings{JJMS:EPEW:10,
author ={L. Jacobsen and M. Jacobsen and M.H. M{\o}ller and J. Srba},
title ={A Framework for Relating Timed Transition Systems and Preserving {TCTL} Model Checking},
booktitle ={Proceedings of the 7th European Performance Engineering Workshop ({EPEW}'10)},
year ={2010},
series ={LNCS},
volume ={6342},
publisher ={Springer-Verlag},
pages ={83--98},
abstract ={ Many formal translations between time dependent models have been proposed over the years. While some of them produce timed bisimilar models, others preserve only reachability or (weak) trace equivalence. We suggest a general framework for arguing when a translation preserves Timed Computation Tree Logic (TCTL) or its safety fragment.The framework works at the level of timed transition systems, making it independent of the modeling formalisms and applicable to many of the translations published in the literature. Finally, we present a novel translation from extended Timed-Arc Petri Nets to Networks of Timed Automata and using the framework argue that itpreserves the full TCTL. The translation has been implemented in the verification tool TAPAAL.},
ee ={http://www.springerlink.com/content/xr33g66627h03110},
pdf ={http://www.brics.dk/~srba/files/JJMS:EPEW:10.pdf},
}

@inproceedings{Srba:CompSysTech:10,
author ={J. Srba},
title ={An Experiment with Using Google Tools for Project Supervision at Tertiary Education},
booktitle ={Proceedings of the 11th International Conference on Computer Systems and Technologies ({CompSysTech}'10)},
year ={2010},
pages ={430--435},
publisher ={ACM},
note ={This is the author's version of the work. It is posted here by the permission of ACM for your personal use. Not for redistribution. The link to the definite version is available below.},
abstract ={Problem oriented project pedagogy is an alternative educational approach which often provides a strong natural motivation for the students' work. On the other hand, it requires certain coordination and cooperation skills in communication inside the project group as well as between the group and its supervisor. We study the use of content and coordination management tools for the support of group work. An experiment using a combination of Google Groups/Docs/Calendar services was carried out at Aalborg University in Denmark and we report here on the outcomes of the trial.},
pdf ={http://www.brics.dk/~srba/files/Srba:CompSysTech:10.pdf},
ee ={http://doi.acm.org/10.1145/1839379.1839455},
}

@inproceedings{BJS:ICFEM:09,
author ={J. Byg and K.Y. J{\o}rgensen and J. Srba},
title ={An Efficient Translation of Timed-Arc {P}etri Nets to Networks of Timed Automata},
booktitle ={Proceedings of the 11th International Conference on Formal Engineering Methods ({ICFEM}'09)},
year ={2009},
series ={LNCS},
volume ={5885},
publisher ={Springer-Verlag},
pages ={698--716},
abstract ={Bounded timed-arc Petri nets with read-arcs were recently proven equivalent to networks of timed automata, though the Petri net model cannot express urgent behaviour and the described mutual trans- lations are rather inefficient. We propose an extension of timed-arc Petri nets with invariants to enforce urgency and with transport arcs to generalise the read-arcs. We also describe a novel translation from the extended timed-arc Petri net model to networks of timed automata. The translation is implemented in the tool TAPAAL and it uses UPPAAL as the verification engine. Our experiments confirm the efficiency of the translation and in some cases the translated models verify significantly faster than the native UPPAAL models do.},
ee ={http://dx.doi.org/10.1007/978-3-642-10373-5_36},
pdf ={http://www.brics.dk/~srba/files/BJS:ICFEM:09.pdf},
}

@inproceedings{AILS:TFM:09,
author ={L. Aceto and A. Ingolfsdottir and K.G. Larsen and J. Srba},
title ={Teaching Concurrency: Theory in Practice},
booktitle ={Proceedings of the 2nd International FME Conference on Teaching Formal Methods ({TFM}'09)},
year ={2009},
series ={LNCS},
volume ={5846},
publisher ={Springer-Verlag},
pages ={158--175},
abstract ={Teaching courses that rely on sound mathematical principles is nowadays a challenging task at many universities. On the one hand there is an increased demand for educating students in these areas, on the other hand there are more and more students being accepted with less adequate skills in mathematics. We report here on our experiences in teaching concurrency theory over the last twenty years or so to students ranging from mathsphobic bachelor students to sophisticated doctoral students. The contents of the courses, the material on which they are based and the pedagogical philosophy underlying them are described, as well as some of the lessons that we have learned over the years. },
ee ={http://dx.doi.org/10.1007/978-3-642-04912-5_11},
pdf ={http://www.brics.dk/~srba/files/AILS:TFM:09.pdf},
}

@inproceedings{BJS:ATVA:09,
author ={J. Byg and K.Y. J{\o}rgensen and J. Srba},
title ={{TAPAAL}: Editor, Simulator and Verifier of Timed-Arc {P}etri Nets},
booktitle ={Proceedings of the 7th International Symposium on Automated Technology for Verification and Analysis ({ATVA}'09)},
year ={2009},
series ={LNCS},
volume ={5799},
publisher ={Springer-Verlag},
pages ={84--89},
abstract ={TAPAAL is a new platform independent tool for modelling, simulation and verification of timed-arc Petri nets. TAPAAL provides a stand-alone editor and simulator, while the verification module translates timed-arc Petri net models into networks of timed automata and uses the UPPAAL engine for the automatic analysis. We report on the status of the first release of TAPAAL (available at http://www.tapaal.net), on its new modelling features and we demonstrate the efficiency and modelling capabilities of the tool on a few examples.},
ee ={http://dx.doi.org/10.1007/978-3-642-04761-9_7},
pdf ={http://www.brics.dk/~srba/files/BJS:ATVA:09.pdf},
}

@inproceedings{BKLS:ICTAC:09,
author ={N. Bene\v{s} and J. K\v{r}et\'{\i}nsk\'{y} and K.G. Larsen and J. Srba},
title ={Checking Thorough Refinement on Modal Transition Systems Is {EXPTIME}-Complete},
booktitle ={Proceedings of the 6th International Colloquium on Theoretical Aspects of Computing ({ICTAC}'09)},
year ={2009},
series ={LNCS},
volume ={5684},
pages ={112--126},
publisher ={Springer-Verlag},
abstract ={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. },
ee ={http://dx.doi.org/10.1007/978-3-642-03466-4_7},
pdf ={http://www.brics.dk/~srba/files/BKLS:ICTAC:09.pdf},
}

@inproceedings{KSSK:FOSSACS:09,
author ={M. K\"{u}hnrich and S. Schwoon and J. Srba and S. Kiefer},
title ={Interprocedural Dataflow Analysis over Weight Domains with Infinite Descending Chains},
booktitle ={Proceedings of the 12th International Conference on Foundations of Software Science and Computational Structures ({FOSSACS}'09)},
publisher ={Springer-Verlag},
series ={LNCS},
volume ={5504},
pages ={440--455},
year ={2009},
abstract ={We study generalized fixed-point equations over idempotent semirings and provide an efficient algorithm for the detection whether a sequence of Kleene's iterations stabilizes after a finite number of steps. Previously known approaches considered only bounded semirings where there are no infinite descending chains. The main novelty of our work is that we deal with semirings without the boundedness restriction. Our study is motivated by several applications from interprocedural dataflow analysis. We demonstrate how the reachability problem for weighted pushdown automata can be reduced to solving equations in the framework mentioned above and we describe a few applications to demonstrate its usability. },
ee ={http://arxiv.org/abs/0901.0501},
pdf ={http://www.brics.dk/~srba/files/KSSK:FOSSACS:09.pdf},
}

@inproceedings{BFLMS:FORMATS:08,
author ={P. Bouyer and U. Fahrenberg and K.G. Larsen and N. Markey and J. Srba},
title ={Infinite Runs in Weighted Timed Automata with Energy Constraints},
booktitle ={Proceedings of the 6th International Conference on Formal Modelling and Analysis of Timed Systems (FORMATS'08)},
year ={2008},
series ={LNCS},
volume ={5215},
pages ={33--47},
publisher ={Springer-Verlag},
abstract ={We study the problems of existence and construction of infinite schedules for finite weighted automata and one-clock weighted timed automata, subject to boundary constraints on the accumulated weight. More specifically, we consider automata equipped with positive and negative weights on transitions and locations, corresponding to the production and consumption of some resource (e.g. energy). We ask the question whether there exists an infinite path for which the accumulated weight for any finite prefix satisfies certain constraints (e.g. remains between 0 and some given upper-bound). We also consider a game version of the above, where certain transitions may be uncontrollable.},
ee ={http://dx.doi.org/10.1007/978-3-540-85778-5_4},
pdf ={http://www.brics.dk/~srba/files/BFLMS:FORMATS:08.pdf},
}

@inproceedings{S:FORMATS:08,
author ={J. Srba},
title ={Comparing the Expressiveness of Timed Automata and Timed Extensions of {P}etri Nets},
booktitle ={Proceedings of the 6th International Conference on Formal Modelling and Analysis of Timed Systems (FORMATS'08)},
year ={2008},
series ={LNCS},
volume ={5215},
pages ={15--32},
publisher ={Springer-Verlag},
abstract ={Time dependant models have been intensively studied for many reasons, among others because of their applications in software verification and due to the development of embedded platforms where reliability and safety depend to a large extent on the time features. Many of the time dependant models were suggested as real-time extensions of several well-known untimed models. The most studied formalisms include Networks of Timed Automata which extend the model of communicating finite-state machines with a finite number of real-valued clocks, and timed extensions of Petri nets where the added time constructs include e.g. time intervals that are assigned to the transitions (Time Petri Nets) or to the arcs (Timed-Arc Petri Nets). In this paper, we shall semi-formally introduce these models, discuss their strengths and weaknesses, and provide an overview of the known results about the relationships among the models.},
ee ={http://dx.doi.org/10.1007/978-3-540-85778-5_3},
pdf ={http://www.brics.dk/~srba/files/S:FORMATS:08.pdf},
note ={The paper makes in Section 3.1 a claim that untimed language equivalence for timed automata is decidable in PSPACE [7]. This claim is wrong as [7] refers only to deterministic systems.},
}

@inproceedings{NS:MFCS:07,
author ={D. Nowotka and J. Srba},
title ={Height-Deterministic Pushdown Automata},
booktitle ={Proceedings of the 32nd International Symposium on Mathematical Foundations of Computer Science (MFCS'07)},
publisher ={Springer-Verlag},
series ={LNCS},
volume ={4708},
year ={2007},
pages ={125--134},
abstract ={We define the notion of height-deterministic pushdown automata, a model where for any given input string the stack heights during any (nondeterministic) computation on the input are a priori fixed. Different subclasses of height-deterministic pushdown automata, strictly containing the class of regular languages and still closed under boolean language operations, are considered. Several of such language classes have been described in the literature. Here, we suggest a natural and intuitive model that subsumes all the formalisms proposed so far by employing height-deterministic pushdown automata. Decidability and complexity questions are also considered.},
ee ={http://dx.doi.org/10.1007/978-3-540-74456-6_13 },
pdf ={http://www.brics.dk/~srba/files/NS:MFCS:07.pdf},
}

@inproceedings{DES:ATVA:06,
author ={G. Delzanno and J. Esparza and J. Srba},
title ={Monotonic Set-Extended Prefix Rewriting and Verification of Recursive Ping-Pong Protocols},
booktitle ={Proceedings of the 4th International Symposium on Automated Technology for Verification and Analysis (ATVA'06)},
year ={2006},
series ={LNCS},
volume ={4218},
pages ={415--429},
publisher ={Springer-Verlag},
abstract ={Ping-pong protocols with recursive definitions of agents, but without any active intruder, are a Turing powerful model. We show that under the environment sensitive semantics (i.e. by adding an active intruder capable of storing all exchanged messages including full analysis and synthesis of messages) some verification problems become decidable. In particular we give an algorithm to decide control state reachability, a problem related to security properties like secrecy and authenticity. The proof is via a reduction to a new prefix rewriting model called Monotonic Set-extended Prefix rewriting (MSP). We demonstrate further applicability of the introduced model by encoding a fragment of the ccp (concurrent constraint programming) language into MSP. },
ee ={http://dx.doi.org/10.1007/11901914_31},
pdf ={http://www.brics.dk/~srba/files/DES:ATVA:06.pdf},
}

@inproceedings{S:CSL:06,
author ={J. Srba},
title ={Visibly Pushdown Automata: From Language Equivalence to Simulation and Bisimulation},
booktitle ={Proceedings of the 15th Annual Conference of the European Association for Computer Science Logic (CSL'06)},
year ={2006},
series ={LNCS},
volume ={4207},
pages ={89--103},
publisher ={Springer-Verlag},
abstract ={We investigate the possibility of (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. },
ee ={http://dx.doi.org/10.1007/11874683_6},
pdf ={http://www.brics.dk/~srba/files/S:CSL:06.pdf},
}

@inproceedings{JS:FOSSACS:06,
author ={P. Jan\v{c}ar and J. Srba},
title ={Undecidability Results for Bisimilarity on Prefix Rewrite Systems},
booktitle ={Proceedings of the 9th International Conference on Foundations of Software Science and Computation Structures (FOSSACS'06)},
publisher ={Springer-Verlag},
series ={LNCS},
volume ={3921},
year ={2006},
pages ={277--291},
abstract ={We answer an open question related to bisimilarity checking on labelled transition systems generated by prefix rewrite rules on words. Stirling (1996, 1998) proved the decidability of bisimilarity for normed pushdown processes. This result was substantially extended by Senizergues (1998, 2005) who showed the decidability for regular (or equational) graphs of finite out-degree (which include unnormed pushdown processes). The question of decidability of bisimilarity for a more general class of so called Type -1 systems (generated by prefix rewrite rules of the form R -a-> w where R is a regular language) was left open; this was repeatedly indicated by both Stirling and Senizergues. Here we answer the question negatively, i.e., we show undecidability of bisimilarity on Type -1 systems, even in the normed case. We complete the picture by considering classes of systems that use rewrite rules of the form w -a-> R and R1 -a-> R2 and show when they yield low undecidability (Pi^0_1-completeness) and when high undecidability (Sigma^1_1-completeness), all with and without the assumption of normedness. },
ee ={http://dx.doi.org/10.1007/11690634_19},
pdf ={http://www.brics.dk/~srba/files/JS:FOSSACS:06.pdf},
}

@inproceedings{S:FSTTCS:05,
author ={J. Srba},
title ={On Counting the Number of Consistent Genotype Assignments for Pedigrees},
booktitle ={Proceedings of the 25th International Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS'05)},
series ={LNCS},
volume ={3821},
year ={2005},
pages ={470--482},
publisher ={Springer-Verlag},
abstract ={Consistency checking of genotype information in pedigrees plays an important role in genetic analysis and for complex pedigrees the computational complexity is critical. We present here a detailed complexity analysis for the problem of counting the number of complete consistent genotype assignments. Our main result is a polynomial time algorithm for counting the number of complete consistent assignments for non-looping pedigrees. We further classify pedigrees according to a number of natural parameters like the number of generations, the number of children per individual and the cardinality of the set of alleles. We show that even if we assume all these parameters as bounded by reasonably small constants, the counting problem becomes computationally hard (#P-complete) for looping pedigrees. The border line for counting problems computable in polynomial time (i.e. belonging to the class FP) and #P-hard problems is completed by showing that even for general pedigrees with unlimited number of generations and alleles but with at most one child per individual and for pedigrees with at most two generations and two children per individual the counting problem is in FP. },
ee ={http://dx.doi.org/10.1007/11590156_38},
pdf ={http://www.brics.dk/~srba/files/S:FSTTCS:05.pdf},
}

@inproceedings{S:ICATPN:05,
author ={J. Srba},
title ={Timed-Arc {P}etri Nets vs. Networks of Timed Automata},
booktitle ={Proceedings of the 26th International Conference on Application and Theory of {P}etri Nets (ICATPN'05)},
series ={LNCS},
volume ={3536},
year ={2005},
pages ={385--402},
publisher ={Springer-Verlag},
abstract ={We establish mutual translations between the classes of 1-safe timed-arc Petri nets (and its extension with testing arcs) and networks of timed automata (and its subclass where every clock used in the guard has to be reset). The presented translations are very tight (up to isomorphism of labelled transition systems with time). This provides a convenient characterization from the theoretical point of view but is not always satisfactory from the practical point of view because of the possible non-polynomial blow up in the size (in the direction from automata to nets). Hence we relax the isomorphism requirement and provide efficient (polynomial time) reductions between networks of timed automata and 1-safe timed-arc Petri nets preserving the answer to the reachability question. This makes our techniques suitable for automatic translation into a format required by tools like UPPAAL and KRONOS. A direct corollary of the presented reductions is a new PSPACE-completeness result for reachability in 1-safe timed-arc Petri nets, reusing the region/zone techniques already developed for timed automata. },
ee ={http://dx.doi.org/10.1007/11494744_22},
pdf ={http://www.brics.dk/~srba/files/S:ICATPN:05.pdf},
}

@inproceedings{HS:SOFSEM:05,
author ={H. H\"{u}ttel and J. Srba},
title ={Recursion vs. Replication in Simple Cryptographic Protocols},
booktitle ={Proceedings of the 31st Annual Conference on Current Trends in Theory and Practice of Informatics (SOFSEM'05)},
publisher ={Springer-Verlag},
series ={LNCS},
volume ={3381},
year ={2005},
pages ={175--184},
abstract ={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. We also show that the extended 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. },
ee ={http://springerlink.metapress.com/content/wx86blpvh1x7r9lt/?p=a1af14e92d8a461c932ba7b74970cfce&pi=20},
pdf ={http://www.brics.dk/~srba/files/HS:SOFSEM:05.pdf},
}

@inproceedings{JS:TCS:04,
author ={P. Jan\v{c}ar and J. Srba},
title ={Highly Undecidable Questions for Process Algebras},
booktitle ={Proceedings of the 3rd IFIP International Conference on Theoretical Computer Science (TCS'04)},
publisher ={Kluwer Academic Publishers},
series ={Exploring New Frontiers of Theoretical Informatics},
year ={2004},
pages ={507--520},
abstract ={We show Sigma^1_1-completeness of weak bisimilarity for PA (process algebra), and of weak simulation preorder/equivalence for PDA (pushdown automata), PA and PN (Petri nets). We also show Pi^1_1-hardness of weak omega-trace equivalence for the (sub)classes BPA (basic process algebra) and BPP (basic parallel processes). },
pdf ={http://www.brics.dk/~srba/files/JS:TCS:04.pdf},
}

@inproceedings{HS:WITS:04,
author ={H. H\"uttel and J. Srba},
title ={Recursive Ping-Pong Protocols},
booktitle ={Proceedings of the 4th International Workshop on Issues in the Theory of Security (WITS'04)},
year ={2004},
pages ={129--140},
abstract ={This paper introduces a process calculus with recursion which allows us to express an unbounded number of runs of the ping-pong protocols introduced by Dolev and Yao. We study the decidability issues associated with two common approaches to checking security properties, namely reachability analysis and bisimulation checking. Our main result is that our channel-free and memory-less calculus is Turing powerful, assuming that at least three principals are involved. We also investigate the expressive power of the calculus in the case of two participants. Here, our main results are that reachability and, under certain conditions, also strong bisimilarity become decidable. },
pdf ={http://www.brics.dk/~srba/files/HS:WITS:04.pdf},
}

@inproceedings{S:INFINITY:03,
author ={J. Srba},
title ={Completeness Results for Undecidable Bisimilarity Problems},
booktitle ={Proceedings of the 5th International Workshop on Verification of Infinite-State Systems (INFINITY'03)},
year ={2004},
pages ={5--19},
volume ={98},
series ={ENTCS},
publisher ={Elsevier Science Publishers},
abstract ={ We establish Sigma_1^1-completeness (in the analytical hierarchy) of weak bisimilarity checking for infinite-state processes generated by pushdown automata and parallel pushdown automata. The results imply Sigma_1^1-completeness of weak bisimilarity for Petri nets and give a negative answer to the open problem stated by Jancar (CAAP'95): ``does the problem of weak bisimilarity for Petri nets belong to Delta_1^1 ?'' },
ee ={http://dx.doi.org/10.1016/j.entcs.2003.10.003},
pdf ={http://www.brics.dk/~srba/files/S:INFINITY:03.pdf},
}

@inproceedings{S:DLT:02,
author ={J. Srba},
title ={Undecidability of Weak Bisimilarity for {PA}-Processes},
booktitle ={Proceedings of the 6th International Conference on Developments in Laguage Theory (DLT'02)},
year ={2003},
series ={LNCS},
volume ={2450},
pages ={197--208},
publisher ={Springer-Verlag},
abstract ={We prove that the problem whether two PA-processes are weakly bisimilar is undecidable. We combine several proof techniques to provide a reduction from Post's correspondence problem to our problem: existential quantification technique, masking technique and deadlock elimination technique. },
ee ={http:dx.doi.org/10.1007/3-540-45005-X_17},
pdf ={http://www.brics.dk/~srba/files/S:DLT:02.pdf},
}

@inproceedings{S:CONCUR:02,
author ={J. Srba},
title ={Undecidability of Weak Bisimilarity for Pushdown Processes},
booktitle ={Proceedings of the 13th International Conference on Concurrency Theory (CONCUR'02)},
year ={2002},
volume ={2421},
series ={LNCS},
pages ={579--593},
publisher ={Springer-Verlag},
abstract ={We prove undecidability of the problem whether a given pair of pushdown processes is weakly bisimilar. We also show that this undecidability result extends to a subclass of pushdown processes satisfying the normedness condition. },
ee ={http://dx.doi.org/10.1007/3-540-45694-5_38 },
pdf ={http://www.brics.dk/~srba/files/S:CONCUR:02.pdf},
}

@inproceedings{S:ICALP:02,
author ={J. Srba},
title ={Strong Bisimilarity and Regularity of Basic Process Algebra is {PSPACE}-Hard},
booktitle ={Proceedings of the 29th International Colloquium on Automata, Languages and Programming (ICALP'02)},
year ={2002},
series ={LNCS},
volume ={2380},
pages ={716--727},
publisher ={Springer-Verlag},
abstract ={Strong bisimilarity and regularity checking problems of Basic Process Algebra (BPA) are decidable, with the complexity upper bounds 2-EXPTIME. On the other hand, no lower bounds were known. In this paper we demonstrate PSPACE-hardness of these problems. },
ee ={http://dx.doi.org/10.1007/3-540-45465-9_61 },
pdf ={http://www.brics.dk/~srba/files/S:ICALP:02.pdf},
}

@inproceedings{S:FOSSACS:02,
author ={J. Srba},
title ={Note on the Tableau Technique for Commutative Transition Systems},
booktitle ={Proceedings of the 5th International Conference on Foundations of Software Science and Computation Structures (FOSSACS'02)},
publisher ={Springer-Verlag},
series ={LNCS},
volume ={2303},
year ={2002},
pages ={387--401},
abstract ={We define a class of transition systems called effective commutative transition systems (ECTS) and show, by generalising a tableau-based proof for BPP, that strong bisimilarity between any two states of such a transition system is decidable. It gives a general technique for extending decidability borders of strong bisimilarity for a wide class of infinite-state transition systems. This is demonstrated for several process formalisms, namely BPP process algebra, lossy BPP processes, BPP systems with interrupt and timed-arc BPP nets. },
ee ={http://dx.doi.org/10.1007/3-540-45931-6_27},
pdf ={http://www.brics.dk/~srba/files/S:FOSSACS:02.pdf},
}

@inproceedings{S:STACS:02,
author ={J. Srba},
title ={Strong Bisimilarity and Regularity of Basic Parallel Processes is {PSPACE}-Hard},
booktitle ={Proceedings of the 19th International Symposium on Theoretical Aspects of Computer Science (STACS'02)},
year ={2002},
series ={LNCS},
volume ={2285},
pages ={535--546},
publisher ={Springer-Verlag},
abstract ={We show that the problem of checking whether two processes definable in the syntax of Basic Parallel Processes (BPP) are strongly bisimilar is PSPACE-hard. We also demonstrate that there is a polynomial time reduction from the strong bisimilarity checking problem of regular BPP to the strong regularity (finiteness) checking of BPP. This implies that strong regularity of BPP is also PSPACE-hard. },
ee ={http://dx.doi.org/10.1007/3-540-45841-7_44},
pdf ={http://www.brics.dk/~srba/files/S:STACS:02.pdf},
}

@inproceedings{NSS:FSTTCS:01,
author ={M. Nielsen and V. Sassone and J. Srba},
title ={Properties of Distributed Timed-Arc {P}etri Nets},
booktitle ={Proceedings of the 21st International Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS'01)},
series ={LNCS},
volume ={2245},
year ={2001},
pages ={280--291},
publisher ={Springer-Verlag},
abstract ={In (Nielsen, Sassone, Srba, ICATPN'01) we started a research on a distributed-timed extension of Petri nets where time parameters are associated with tokens and arcs carry constraints that qualify the age of tokens required for enabling. This formalism enables to model e.g. hardware architectures like GALS. We give a formal definition of process semantics for our model and investigate several properties of local versus global timing: expressiveness, reachability and coverability. },
ee ={http://dx.doi.org/10.1007/3-540-45294-X_24},
pdf ={http://www.brics.dk/~srba/files/NSS:FSTTCS:01.pdf},
}

@inproceedings{S:CONCUR:01,
author ={J. Srba},
title ={On the Power of Labels in Transition Systems},
booktitle ={Proceedings of the 12th International Conference on Concurrency Theory (CONCUR'01)},
publisher ={Springer-Verlag},
series ={LNCS},
volume ={2154},
year ={2001},
pages ={277--291},
abstract ={In this paper we discuss the role of labels in transition systems with regard to bisimilarity and model checking problems. We suggest a general reduction from labelled transition systems to unlabelled ones, preserving bisimilarity and satisfiability of mu-calculus formulas. We apply the reduction to the class of transition systems generated by Petri nets and pushdown automata, and obtain several decidability/complexity corollaries for unlabelled systems. Probably the most interesting result is undecidability of strong bisimilarity for unlabelled Petri nets. },
ee ={http://dx.doi.org/10.1007/3-540-44685-0_19},
pdf ={http://www.brics.dk/~srba/files/S:CONCUR:01.pdf},
}

@inproceedings{NSS:ICATPN:01,
author ={M. Nielsen and V. Sassone and J. Srba},
title ={Towards a Notion of Distributed Time for {P}etri nets},
booktitle ={Proceedings of the 22nd International Conference on Application and Theory of {P}etri Nets (ICATPN'01)},
series ={LNCS},
volume ={2075},
year ={2001},
pages ={23--31},
publisher ={Springer-Verlag},
abstract ={We set the ground for research on a timed extension of Petri nets where time parameters are associated with tokens and arcs carry constraints that qualify the age of tokens required for enabling. The novelty is that, rather than a single global clock, we use a set of unrelated clocks --- possibly one per place --- allowing a local timing as well as distributed time synchronisation. We give a formal definition of the model and investigate properties of local versus global timing, including decidability issues and notions of processes of the respective models. },
ee ={http://dx.doi.org/10.1007/3-540-45740-2_3},
pdf ={http://www.brics.dk/~srba/files/NSS:ICATPN:01.pdf},
}

@inproceedings{S:EXPRESS:00,
author ={J. Srba},
title ={Complexity of Weak Bisimilarity and Regularity for {BPA} and {BPP}},
booktitle ={Proceedings of the 7th International Workshop on Expressiveness in Concurrency (EXPRESS'00)},
publisher ={Elsevier Science Publishers},
series ={ENTCS},
volume ={39},
number ={1},
year ={2000},
abstract ={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 have been demonstrated by Stribrna.. Mayr achieved recently a result, saying that weak bisimilarity for BPP is Pi_2^P-hard. 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 Pi_2^P-hardness result 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. },
ee ={http://dx.doi.org/10.1016/S1571-0661(05)82505-8},
pdf ={http://www.brics.dk/~srba/files/S:EXPRESS:00.pdf},
}

@inproceedings{KS:MFCS:00,
author ={O. Kl\'{\i}ma and J. Srba},
title ={Matching Modulo Associativity and Idempotency is {NP}-Complete},
booktitle ={Proceedings of the 25rd International Symposium on Mathematical Foundations of Computer Science (MFCS'00)},
publisher ={Springer-Verlag},
series ={LNCS},
volume ={1893},
year ={2000},
pages ={456--466},
abstract ={We show that AI-matching (AI denotes the theory of an associative and idempotent function symbol), which is solving matching word equations in free idempotent semigroups, is NP-complete.},
ee ={http://dx.doi.org/10.1007/3-540-44612-5_41 },
pdf ={http://www.brics.dk/~srba/files/KS:MFCS:00.pdf},
}

@inproceedings{CKS:SOFSEM:99,
author ={I. \v{C}ern\'{a} and O. Kl\'{\i}ma and J. Srba},
title ={Pattern Equations and Equations with Stuttering},
booktitle ={Proceedings of the 26th Annual Conference on Current Trends in Theory and Practice of Informatics (SOFSEM'99)},
publisher ={Springer-Verlag},
series ={LNCS},
volume ={1725},
year ={1999},
pages ={369--378},
abstract ={Word equation in a special form X=A, where X is a sequence of variables and A is a sequence of constants, is considered. The problem whether X=A has a solution over a free monoid is shown to be NP-complete. It is also shown that disjunction of a special type equation systems and conjunction of the general ones can be eliminated. Finally, the case of stuttering equations where the word identity is read modulo xx=x is mentioned. },
ee ={http://dx.doi.org/10.1007/3-540-47849-3_24},
pdf ={http://www.brics.dk/~srba/files/CKS:SOFSEM:99.pdf},
}

@inproceedings{S:MFCS:98,
author ={J. Srba},
title ={Deadlocking States in Context-Free Process Algebra},
booktitle ={Proceedings of the 23rd International Symposium on Mathematical Foundations of Computer Science (MFCS'98)},
publisher ={Springer-Verlag},
series ={LNCS},
volume ={1450},
year ={1998},
pages ={388--398},
abstract ={Recently the class of BPA (or context-free) processes has been intensively studied and bisimilarity and regularity appeared to be decidable. We extend these processes with a deadlocking state into BPAd systems. Bosscher has proved that bisimilarity and regularity remain decidable. We generalise his approach introducing strict and nonstrict version of bisimilarity. We show that the BPAd class is more expressive w.r.t. (both strict and nonstrict) bisimilarity but it remains language equivalent to BPA. Finally we give a characterization of those BPAd processes which can be equivalently (up to bisimilarity) described within the pure BPA syntax. },
ee ={http://www.springerlink.com/content/34cwwhqwuulnr22p/},
pdf ={http://www.brics.dk/~srba/files/S:MFCS:98.pdf},
}

@book{AILS:reactive:07,
author ={L. Aceto and A. Ingolfsdottir and K.G. Larsen and J. Srba},
title ={Reactive Systems: Modelling, Specification and Verification},
publisher ={Cambridge University Press},
pages ={1--300},
year ={2007},
abstract ={Formal methods is the term used to describe the specification and verification of software and software systems using mathematical logic. Various methodologies have been developed and incorporated into software tools. An important subclass is distributed systems. There are many books that look at particular methodologies for such systems, e.g. CSP, process algebra. This book offers a more balanced introduction for graduate students that describes the various approaches, their strengths and weaknesses, and when they are best used. Milner's CCS and its operational semantics are introduced, together with notions of behavioural equivalence based on bisimulation techniques and with variants of Hennessy-Milner modal logics. Later in the book, the presented theories are extended to take timing issues into account. The book has arisen from various courses taught in Iceland and Denmark and is designed to give students a broad introduction to the area, with exercises throughout. },
ee ={http://www.cambridge.org/uk/catalogue/catalogue.asp?isbn=9780521875462},
}

@inbook{AIS:BookChapter:11,
author ={L. Aceto and A. Ingolfsdottir and J. Srba},
title ={Advanced Topics in Bisimulation and Coinduction},
chapter ={The Algorithmics of Bisimilarity},
publisher ={Cambridge University Press},
year ={2011},
pages ={100--172},
ee ={http://www.cambridge.org/gb/knowledge/isbn/item6542021},
}

@inbook{LRS:BookChapter:09,
author ={D. Lime and O.H. Roux and J. Srba},
title ={Communicating Embedded Systems - Software and Design},
chapter ={Models for Embedded Real-Time Systems},
publisher ={ISTE Publishing/John Wiley},
year ={2009},
pages ={1--38},
ee ={http://www.iste.co.uk/index.php?f=x&ACTION=View&id=288},
}

@inbook{Detal:BookChapter:09,
author ={A. David and G. Behrmann and P. Bulychev and J. Byg and T. Chatain and K.G. Larsen and P. Pettersson and J.I. Rasmussen and J. Srba and W. Yi and K.Y. J{\o}rgensen and D. Lime and M. Magnin and O.H. Roux and L.-M. Traonouez},
title ={Communicating Embedded Systems - Software and Design},
chapter ={Tools for Model-Checking Timed Systems},
publisher ={ISTE Publishing/John Wiley},
year ={2009},
ee ={http://www.iste.co.uk/index.php?f=x&ACTION=View&id=288},
}

@inbook{S:Roadmap:04,
author ={Jiri Srba},
title ={Current Trends in Theoretical Computer Science, The Challenge of the New Century},
chapter ={Roadmap of Infinite Results},
publisher ={World Scientific Publishing Co.},
year ={2004},
volume ={2},
pages ={337--350},
note ={Updated version of the EATCS Bulletin contribution. See also EE for an updated on-line version.},
abstract ={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.},
ee ={http://www.brics.dk/~srba/roadmap},
}

@article{BJLLS:MSCS:11,
title ={Model-Checking Web Services Business Activity Protocols},
author ={A.P. Marques Jr. and A.P. Ravn and J. Srba and S. Vighio},
journal ={Software Tools for Technology Transfer (STTT)},
publisher ={Springer-Verlag},
year ={2012},
volume ={},
number ={},
pages ={1--23},
note ={To appear.},
abstract ={Web Services Business Activity specification defines two 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 distributed applications. In order to verify fundamental properties of the protocols we 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 we translate this format into a network of communicating state machines directly suitable for verification in UPPAAL.Our results show that the WS-BA protocols, as described in the standard specification, 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 further investigation of the modified protocols suggests that in case of the BAwCC protocol messages should be 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 protocols is that all parties always reach, under certain fairness assumptions, their final states. Based on an automatic verification with different communication models, we prove that our enhanced protocols satisfy this property whereas the original protocols do not.All verification results presented in this article were performedin a fully automatic way using our new tool csv2uppaal.},
pdf ={http://www.brics.dk/~srba/files/MRSV:sttt:2012.pdf},
}

@article{BJLLS:MSCS:12,
title ={Extending Modal Transition Systems with Structured Labels},
author ={S.S. Bauer and L. Juhl and K.G. Larsen and A. Legay and J. Srba},
journal ={Mathematical Structures in Computer Science},
publisher ={Cambridge University Press},
year ={2012},
volume ={},
number ={},
pages ={1--35},
note ={To appear.},
abstract ={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.},
pdf ={http://www.brics.dk/~srba/files/BJLLS:MSCS:12.pdf},
}

@article{JLS:JLAP:12,
title ={Modal Transition Systems with Weight Intervals},
author ={L. Juhl and K.G. Larsen and J. Srba},
journal ={Journal of Logic and Algebraic Programming},
publisher ={Elsevier},
year ={2012},
volume ={81},
number ={4},
pages ={408--421},
abstract ={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.},
pdf ={http://www.brics.dk/~srba/files/JLS:JLAP:12.pdf},
}

@article{BKLS:TCS:09,
title ={On Determinism in Modal Transition Systems},
author ={N. Bene\v{s} and J. K\v{r}et\'{\i}nsk\'{y} and K.G. Larsen and J. Srba},
journal ={Theoretical Computer Science},
publisher ={Elsevier},
year ={2009},
volume ={410},
number ={41},
pages ={4026--4043},
abstract ={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.},
ee ={http://dx.doi.org/10.1016/j.tcs.2009.06.009},
pdf ={http://www.brics.dk/~srba/files/BKLS:TCS:09.pdf},
}

@article{S:LMCS:09,
author ={J. Srba},
title ={Beyond Language Equivalence on Visibly Pushdown Automata},
journal ={Logical Methods in Computer Science},
publisher ={Creative Commons},
volume ={5},
number ={1:2},
pages ={1--22},
year ={2009},
abstract ={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.},
ee ={http://dx.doi.org/10.2168/LMCS-5%281%3A2%292009},
pdf ={http://arxiv.org/pdf/0901.2068v2},
}

@article{JS:JACM:08,
author ={P. Jan\v{c}ar and J. Srba},
title ={Undecidability of Bisimilarity by Defender's Forcing},
journal ={Journal of the ACM},
volume ={55},
number ={1},
year ={2008},
pages ={1--26},
publisher ={ACM},
address ={New York, NY, USA},
abstract ={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.},
ee ={http://doi.acm.org/10.1145/1326554.1326559},
pdf ={http://www.brics.dk/~srba/files/JS:JACM:08.pdf},
}

@article{HS:JAR:05,
author ={H. H\"{u}ttel and J. Srba},
title ={Decidability Issues for Extended Ping-Pong Protocols},
journal ={Journal of Automated Reasoning},
volume ={36},
number ={1--2},
pages ={125--147},
year ={2006},
publisher ={Kluwer Academic Publishers},
abstract ={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.},
ee ={http://dx.doi.org/10.1007/s10817-005-9015-9},
pdf ={http://www.brics.dk/~srba/files/HS:JAR:05},
}

@article{MSS:IC:04,
author ={F. Moller and S.A. Smolka and J. Srba},
title ={On the Computational Complexity of Bisimulation, Redux},
journal ={Information and Computation},
volume ={192},
number ={2},
pages ={129--143},
year ={2004},
publisher ={Elsevier Science},
abstract ={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.},
ee ={http://dx.doi.org/10.1016/j.ic.2004.06.003},
pdf ={http://www.brics.dk/~srba/files/MSS:IC:04.pdf},
}

@article{S:EATCS:02,
author ={J. Srba},
title ={Roadmap of Infinite Results},
journal ={Bulletin of the European Association for Theoretical Computer Science, Columns: Concurrency},
volume ={78},
pages ={163--175},
year ={2002},
abstract ={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.},
ee ={http://www.brics.dk/~srba/roadmap},
}

@article{S:ACTA:2003,
author ={J. Srba},
title ={Strong Bisimilarity of Simple Process Algebras: Complexity Lower Bounds},
journal ={Acta Informatica},
volume ={39},
pages ={469--499},
year ={2003},
publisher ={Springer-Verlag},
abstract ={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.},
ee ={http://www.springerlink.com/content/kd9yp238c4a5p7t1/},
pdf ={http://www.brics.dk/~srba/files/S:ACTA:03.pdf},
}

@article{JNS:02:IC,
author ={M. Jurdzinski and M. Nielsen and J. Srba},
title ={Undecidability of Domino Games and Hhp-Bisimilarity},
journal ={Information and Computation},
volume ={184},
number ={2},
pages ={343--368},
year ={2003},
publisher ={Elsevier Science},
abstract ={ 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. },
ee ={http://dx.doi.org/10.1016/S0890-5401(03)00064-6},
pdf ={http://www.brics.dk/~srba/files/JNS:IC:02.pdf},
}

@article{S:MSCS:02,
title ={Complexity of Weak Bisimilarity and Regularity for BPA and BPP},
author ={J. Srba},
pages ={567--587},
journal ={Mathematical Structures in Computer Science},
year ={2003},
volume ={13},
publisher ={Cambridge University Press},
abstract ={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. },
ee ={http://dx.doi.org/10.1017/S0960129503003992},
pdf ={http://www.brics.dk/~srba/files/S:MSCS:02.pdf},
}

@article{S:TCS:01,
author ={J. Srba},
title ={Basic Process Algebra with Deadlocking States},
journal ={Theoretical Computer Science},
publisher ={Elsevier},
volume ={266},
number ={1--2},
pages ={605--630},
year ={2001},
abstract ={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. },
ee ={http://dx.doi.org/10.1016/S0304-3975(00)00290-5},
pdf ={http://www.brics.dk/~srba/files/S:TCS:01.pdf},
}

@techreport{BKLMS:TechRep:12,
author ={N. Bene\v{s} and J. K\v{r}et\'{\i}nsk\'{y} and K.G. Larsen and M.H. M{\o}ller and J. Srba},
title ={Dual-Priced Modal Transition Systems with Time Durations},
institution ={Faculty of Informatics MU},
year ={2012},
number ={FIMU-RS-2012-01},
key ={FIMU-RS-2012-01},
pagecount ={23},
ee ={http://www.fi.muni.cz/reports/2012/abstract/FIMU-RS-2012-01.shtml},
abstract ={Modal transition systems are a well-established specification formalism for a high-level modelling of component-based software systems. We present a novel extension of the formalism called modal transition systems with durations where time durations are modelled as controllable or uncontrollable intervals. We further equip the model with two kinds of quantitative aspects: each action has its own running cost per time unit, and actions may require several hardware components of different costs. We ask the question, given a fixed budget for the hardware components, what is the implementation with the cheapest long-run average reward. We give an algorithm for computing such optimal implementations via a reduction to a new extension of mean payoff games with time durations and analyse the complexity of the algorithm.},
}

@techreport{BKLMS:TechRep:11,
author ={N. Bene\v{s} and J. K\v{r}et\'{\i}nsk\'{y} and K.G. Larsen and M.H. M{\o}ller and J. Srba},
title ={Parametric Modal Transition Systems},
institution ={Faculty of Informatics MU},
year ={2011},
number ={FIMU-RS-2011-03},
key ={FIMU-RS-2011-03},
pagecount ={24},
ee ={http://www.fi.muni.cz/reports/2011/abstract/FIMU-RS-2011-03.shtml},
abstract ={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 overcome many of the limitations and we investigate the computational complexity of modal refinement checking. },
}

@techreport{JJMS:TechRep:10,
author ={L. Jacobsen and M. Jacobsen and M.H. M{\o}ller and J. Srba},
title ={A Framework for Relating Timed Transition Systems and Preserving TCTL Model Checking},
institution ={Faculty of Informatics MU},
year ={2010},
number ={FIMU-RS-2010-09},
key ={FIMU-RS-2010-09},
pagecount ={34},
ee ={http://www.fi.muni.cz/reports/2010/abstract/FIMU-RS-2010-09.shtml},
abstract ={Many formal translations between time dependent models have been proposed over the years. While some of them produce timed bisimilar models, others preserve only reachability or (weak) trace equivalence. We suggest a general framework for arguing when a translation preserves Timed Computation Tree Logic (TCTL) or its safety fragment. The framework works at the level of timed transition systems, making it independent of the modeling formalisms and applicable to many of the translations published in the literature. Finally, we present a novel translation from extended Timed-Arc Petri Nets to Networks of Timed Automata and using the framework argue that it preserves the full TCTL. The translation has been implemented in the verification tool TAPAAL.},
}

@techreport{BJS:TechRep:09,
author ={J. Byg and K.Y. J{\o}rgensen and J. Srba},
title ={An Efficient Translation of Timed-Arc {P}etri Nets to Networks of Timed Automata},
institution ={Faculty of Informatics MU},
year ={2009},
number ={FIMU-RS-2009-06},
key ={FIMU-RS-2009-06},
pagecount ={29},
ee ={http://www.fi.muni.cz/reports/2009/abstract/FIMU-RS-2009-06.shtml},
abstract ={Bounded timed-arc Petri nets with read-arcs were recently proven equivalent to net- works of timed automata, though the Petri net model cannot express urgent be- haviour and the described mutual translations are rather inefficient. We propose an extension of timed-arc Petri nets with invariants to enforce urgency and with transport arcs to generalise the read-arcs. We also describe a novel translation from the extended timed-arc Petri net model to networks of timed automata. The trans- lation is implemented in the tool TAPAAL and it uses UPPAAL as the verification engine. Our experiments confirm the efficiency of the translation and in some cases the translated models verify significantly faster than the native UPPAAL models do.},
}

@techreport{BKLS:TechRep:09,
author ={N. Bene\v{s} and J. K\v{r}et\'{\i}nsk\'{y} and K.G. Larsen and J. Srba},
title ={Checking Thorough Refinement on Modal Transition Systems is EXPTIME-Complete},
institution ={Faculty of Informatics MU},
year ={2009},
number ={FIMU-RS-2009-03},
key ={FIMU-RS-2009-03},
pagecount ={28},
ee ={http://www.fi.muni.cz/reports/2009/abstract/FIMU-RS-2009-03.shtml},
abstract ={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.},
}

@techreport{KSchSK:TechRep:09,
author ={M. K\"{u}hnrich and S. Schwoon and J. Srba and S. Kiefer},
title ={Interprocedural Dataflow Analysis over Weight Domains with Infinite Descending Chains},
institution ={arXiv.org open access e-prints in Computer Science},
year ={2009},
number ={arXiv.org 0901.0501},
key ={arXiv.org 0901.0501},
pagecount ={19},
ee ={http://arxiv.org/abs/0901.0501},
abstract ={We study generalized fixed-point equations over idempotent semirings and provide an efficient algorithm for the detection whether a sequence of Kleene's iterations stabilizes after a finite number of steps. Previously known approaches considered only bounded semirings where there are no infinite descending chains. The main novelty of our work is that we deal with semirings without the boundedness restriction. Our study is motivated by several applications from interprocedural dataflow analysis. We demonstrate how the reachability problem for weighted pushdown automata can be reduced to solving equations in the framework mentioned above and we describe a few applications to demonstrate its usability.},
}

@techreport{BFLMS:TechRep:08,
author ={P. Bouyer and U. Fahrenberg and K.G. Larsen and N. Markey and J. Srba},
title ={Infinite Runs in Weighted Timed Automata with Energy Constraints},
institution ={Laboratoire Specification et Verification, ENS Cachan},
year ={2008},
number ={LSV-08-23},
key ={LSV-08-23},
pagecount ={24},
ee ={http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2008-23.pdf},
pdf ={http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2008-23.pdf},
abstract ={We study the problems of existence and construction of infinite schedules for finite weighted automata and one-clock weighted timed automata, subject to boundary constraints on the accumulated weight. More specifically, we consider automata equipped with positive and negative weights on transitions and locations, corresponding to the production and consumption of some resource (e.g. energy). We ask the question whether there exists an infinite path for which the accumulated weight for any finite prefix satisfies certain constraints (e.g. remains between 0 and some given upper-bound). We also consider a game version of the above, where certain transitions may be uncontrollable.},
}

@techreport{ENS:TechRep:07,
author ={J. Esparza and D. Nowotka and J. Srba},
title ={Deterministic Context-Free Model Checking},
institution ={Stuttgart University},
year ={2007},
key ={Stuttgart},
pagecount ={20},
ee ={http://www.fmi.uni-stuttgart.de/szs/publications/info/nowotkdk.dcfmc.shtml},
abstract ={Regular Model-Checking (RMC) is a technique for the formal verification of infinite state systems based on the theory of regular languages. In the paper "Beyond Regular Model Checking" Fisman and Pnueli have shown that RMC can be extended to languages accepted by cascade products of single-state deterministic pushdown automata and finite automata. In this paper we further extend RMC to arbitrary deterministic context-free languages. For this purpose, and inspired by recent results of Caucal, we introduce height-deterministic pushdown automata and show that they satisfy adequate closure properties.},
note ={Note: the nonregular model-checking algorithm works in fact trivially also for any context-free language.},
}

@techreport{DES:TechRep:06,
author ={G. Delzanno and J. Esparza and J. Srba},
title ={Monotonic Set-Extended Prefix Rewriting and Verification of Recursive Ping-Pong Protocols},
institution ={BRICS Research Series},
year ={2006},
number ={RS-06-14},
key ={RS-06-14},
pagecount ={31},
ee ={http://www.brics.dk/RS/06/14/index.html},
abstract ={Ping-pong protocols with recursive definitions of agents, but without any active intruder, are a Turing powerful model. We show that under the environment sensitive semantics (i.e. by adding an active intruder capable of storing all exchanged messages including full analysis and synthesis of messages) some verification problems become decidable. In particular we give an algorithm to decide control state reachability, a problem related to security properties like secrecy and authenticity. The proof is via a reduction to a new prefix rewriting model called Monotonic Set-extended Prefix rewriting (MSP). We demonstrate further applicability of the introduced model by encoding a fragment of the ccp (concurrent constraint programming) language into MSP.},
}

@techreport{S:TechRep:06,
author ={J. Srba},
title ={Visibly Pushdown Automata: From Language Equivalence to Simulation and Bisimulation},
institution ={BRICS Research Series},
year ={2006},
number ={RS-06-13},
key ={RS-06-13},
pagecount ={21},
ee ={http://www.brics.dk/RS/06/13/index.html},
abstract ={We investigate the possibility of (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.},
}

@techreport{JS:TechRep:06,
author ={P. Jan\v{c}ar and J. Srba},
title ={Undecidability Results for Bisimilarity on Prefix Rewrite Systems},
institution ={BRICS Research Series},
year ={2006},
number ={RS-06-7},
key ={RS-06-7},
pagecount ={20},
ee ={http://www.brics.dk/RS/06/7/index.html},
abstract ={We answer an open question related to bisimilarity checking on labelled transition systems generated by prefix rewrite rules on words. Stirling (1996, 1998) proved the decidability of bisimilarity for normed pushdown processes. This result was substantially extended by Sénizergues (1998, 2005) who showed the decidability for regular (or equational) graphs of finite out-degree (which include unnormed pushdown processes). The question of decidability of bisimilarity for a more general class of so called Type -1 systems (generated by prefix rewrite rules of the form R -a-> w where R is a regular language) was left open; this was repeatedly indicated by both Stirling and Sénizergues. Here we answer the question negatively, i.e., we show undecidability of bisimilarity on Type -1 systems, even in the normed case. We complete the picture by considering classes of systems that use rewrite rules of the form w -a-> R and R1 -a-> R2 and show when they yield low undecidability (Pi^0_1-completeness) and when high undecidability (Sigma^1_1-completeness), all with and without the assumption of normedness.},
}

@techreport{S:TechRep:05,
author ={J. Srba},
title ={On Counting the Number of Consistent Genotype Assignments for Pedigrees},
institution ={BRICS Research Series},
year ={2005},
number ={RS-05-28},
key ={RS-05-28},
pagecount ={15},
ee ={http://www.brics.dk/RS/05/28/index.html},
abstract ={Consistency checking of genotype information in pedigrees plays an important role in genetic analysis and for complex pedigrees the computational complexity is critical. We present here a detailed complexity analysis for the problem of counting the number of complete consistent genotype assignments. Our main result is a polynomial time algorithm for counting the number of complete consistent assignments for non-looping pedigrees. We further classify pedigrees according to a number of natural parameters like the number of generations, the number of children per individual and the cardinality of the set of alleles. We show that even if we assume all these parameters as bounded by reasonably small constants, the counting problem becomes computationally hard (#P-complete) for looping pedigrees. The border line for counting problems computable in polynomial time (i.e. belonging to the class FP) and #P-hard problems is completed by showing that even for general pedigrees with unlimited number of generations and alleles but with at most one child per individual and for pedigrees with at most two generations and two children per individual the counting problem is in FP.},
}

@techreport{HS:TechRep:04,
author ={H. H\"{u}ttel and J. Srba},
title ={Recursion vs. Replication in Simple Cryptographic Protocols},
institution ={BRICS Research Series},
year ={2004},
number ={RS-04-23},
key ={RS-04-23},
pagecount ={26},
ee ={http://www.brics.dk/RS/04/23/index.html},
abstract ={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. We also show that the extended 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.},
}

@techreport{JS:TechRep:04,
author ={P. Jan\v{c}ar and J. Srba},
title ={Highly Undecidable Questions for Process Algebras},
institution ={BRICS Research Series},
year ={2004},
number ={RS-04-8},
key ={RS-04-8},
pagecount ={25},
ee ={http://www.brics.dk/RS/04/8/index.html},
abstract ={We show Sigma^1_1-completeness of weak bisimilarity for PA (process algebra), and of weak simulation preorder/equivalence for PDA (pushdown automata), PA and PN (Petri nets). We also show Pi^1_1-hardness of weak omega-trace equivalence for the (sub)classes BPA (basic process algebra) and BPP (basic parallel processes).},
}

@techreport{HS:TechRep:04b,
author ={H. H\"{u}ttel and J. Srba},
title ={Recursive Ping-Pong Protocols},
institution ={BRICS Research Series},
year ={2004},
number ={RS-03-47},
key ={RS-03-47},
pagecount ={21},
ee ={http://www.brics.dk/RS/03/47/index.html},
abstract ={This paper introduces a process calculus with recursion which allows us to express an unbounded number of runs of the ping-pong protocols introduced by Dolev and Yao. We study the decidability issues associated with two common approaches to checking security properties, namely reachability analysis and bisimulation checking. Our main result is that our channel-free and memory-less calculus is Turing powerful, assuming that at least three principals are involved. We also investigate the expressive power of the calculus in the case of two participants. Here, our main results are that reachability and, under certain conditions, also strong bisimilarity become decidable.},
}

@techreport{S:TechRep:02,
author ={J. Srba},
title ={Strong Bisimilarity of Simple Process Algebras: Complexity Lower Bounds},
institution ={BRICS Research Series},
year ={2002},
number ={RS-02-16},
key ={RS-02-16},
pagecount ={33},
ee ={http://www.brics.dk/RS/02/16/index.html},
abstract ={In this paper we study bisimilarity problems for simple process algebras. In particular, we show PSPACE-hardness of the following problems: 1. strong bisimilarity of Basic Parallel Processes (BPP), 2. strong bisimilarity of Basic Process Algebra (BPA), 3. strong regularity of BPP, and 4. strong regularity of BPA. We also demonstrate NL-hardness of strong regularity problems for the normed subclasses of BPP and BPA. Bisimilarity problems for 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.},
}

@techreport{Srba:TechRep:01,
author ={J. Srba},
title ={Note on the Tableau Technique for Commutative Transition Systems},
institution ={BRICS Research Series},
year ={2001},
number ={RS-01-50},
key ={RS-01-50},
pagecount ={19},
ee ={http://www.brics.dk/RS/01/50/index.html},
abstract ={We define a class of transition systems called effective commutative transition systems (ECTS) and show, by generalising a tableau-based proof for BPP, that bisimilarity between any two states of such a transition system is decidable. It gives a general technique for extending decidability borders of strong bisimilarity for a wide class of infinite-state transition systems. This is demonstrated for several process formalisms, namely BPP process algebra, lossy BPP processes, BPP systems with interrupt and timed-arc BPP nets.},
}

@techreport{S:TechRep:01b,
author ={J. Srba},
title ={On the Power of Labels in Transition Systems},
institution ={BRICS Research Series},
year ={2001},
number ={RS-01-19},
key ={RS-01-19},
pagecount ={22},
ee ={http://www.brics.dk/RS/01/19/index.html},
abstract ={In this paper we discuss the role of labels in transition systems with regard to bisimilarity and model checking problems. We suggest a general reduction from labelled transition systems to unlabelled ones, preserving bisimilarity and satisfiability of mu-calculus formulas. We apply the reduction to the class of transition systems generated by Petri nets and pushdown automata, and obtain several decidability/complexity corollaries for unlabelled systems. Probably the most interesting result is undecidability of strong bisimilarity for unlabelled Petri nets.},
}

@techreport{S:TechRep:00,
author ={J. Srba},
title ={Complexity of Weak Bisimilarity and Regularity for BPA and BPP},
institution ={BRICS Research Series},
year ={2000},
number ={RS-00-16},
key ={RS-00-16},
pagecount ={20},
ee ={http://www.brics.dk/RS/00/16/index.html},
abstract ={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 have been demonstrated by Stribrna. Mayr achieved recently a result, saying that weak bisimilarity for BPP is Pi_2^P-hard. 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 Pi_2^P-hardness result 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 co-NP-hardness. In each of the bisimulation/regularity problems we consider also the classes of normed processes},
}

@techreport{KS:TechRep:00,
author ={O. Kl\'{\i}ma and J. Srba},
title ={Matching Modulo Associativity and Idempotency is NP-Complete},
institution ={BRICS Research Series},
year ={2000},
number ={RS-00-13},
key ={RS-00-13},
pagecount ={19},
ee ={http://www.brics.dk/RS/00/13/index.html},
abstract ={We show that AI-matching (AI denotes the theory of an associative and idempotent function symbol), which is solving matching word equations in free idempotent semigroups, is NP-complete.},
}

@techreport{KS:TechRep:99,
author ={O. Kl\'{\i}ma and J. Srba},
title ={Complexity Issues of the Pattern Equations in Idempotent Semigroups},
institution ={Faculty of Informatics MU},
year ={1999},
number ={FIMU-RS-99-02},
key ={FIMU-RS-99-02},
pagecount ={14},
ee ={http://www.fi.muni.cz/reports/1999/abstract/FIMU-RS-99-02.shtml},
abstract ={A pattern equation is a word equation of the form X=A where X is a sequence of variables and A is a sequence of constants. The problem whether X=A has a solution in a free idempotent semigroup (free band) is shown to be NP--complete.},
}

@techreport{CKS:TechRep:99,
author ={I. \v{C}ern\'{a} and O. Kl\'{\i}ma and J. Srba},
title ={On the Pattern Equations},
institution ={Faculty of Informatics MU},
year ={1999},
number ={FIMU-RS-99-01},
key ={FIMU-RS-99-01},
pagecount ={11},
ee ={http://www.fi.muni.cz/reports/1999/abstract/FIMU-RS-99-01.shtml},
abstract ={Word equation in a special form X=A, where X is a sequence of variables and A is a sequence of constants, is considered. The problem whether X=A has a solution over a free monoid (PATTERN EQUATION problem) is shown to be NP--complete. It is also shown that disjunction of a special type equation systems and conjunction of the general ones can be eliminated. Finally, the case of stuttering equations where the word identity is read modulo xx=x is mentioned.},
}

@techreport{S:TechRep:98,
author ={J. Srba},
title ={Comparing the Classes BPA and BPA with Deadlocks},
institution ={Faculty of Informatics MU},
year ={1998},
number ={FIMU-RS-98-05},
key ={FIMU-RS-98-05},
pagecount ={36},
ee ={http://www.fi.muni.cz/reports/1998/abstract/FIMU-RS-98-05.shtml},
abstract ={The class of BPA (or context-free) processes has been intensively studied and bisimilarity and regularity appeared to be decidable. We extend these processes with a deadlocking state into BPA_delta systems. We show that the BPA_delta class is more expressive w.r.t. bisimulation equivalence but it remains language equivalent to BPA. We prove that bisimilarity and regularity remain decidable in the BPA_delta class. Finally we give a characterisation of those BPA_delta processes which can be equivalently (up to bisimilarity) described within the "pure" BPA syntax.},
}

@phdthesis{Srba:thesis:BRICS:03,
author ={J. Srba},
title ={Decidability and Complexity Issues for Infinite-State Processes},
school ={BRICS, Department of Computer Science, University of Aarhus, Denmark},
year ={2003},
pagecount ={171},
note ={Supervisor: Mogens Nielsen, Examiners: Petr Jan\v{c}ar and Colin Stirling.},
pdf ={http://www.brics.dk/~srba/files/thesis.pdf},
}

@phdthesis{Srba:thesis:FIMU:03,
author ={J. Srba},
title ={Selected Techniques for Verification of Infinite-State Processes},
school ={Faculty of Informatics, Masaryk University, Czech Republic},
year ={2005},
pagecount ={124},
note ={Supervisor: Mojm\'{\i}r K\v{r}et\'{\i}nsk\'{y}, Examiners: Milan \v{C}e\v{s}ka and Anton\'{\i}n Ku\v{c}era.},
pdf ={http://www.brics.dk/~srba/files/thesis-brno.pdf},
}

@mastersthesis{Srba:master:98,
author ={J. Srba},
title ={Context-Free Process Algebras Extended with Deadlocks},
school ={Faculty of Informatics, Masaryk University, Brno, Czech Republic},
year ={1998},
pagecount ={42},
note ={Examiners: Ivana Cerna (supervisor) and Antonin Kucera.},
pdf ={http://www.brics.dk/~srba/files/Srba:master:98.pdf},
}

@proceedings{SS:infinity:05,
author ={J. Srba and S.A. Smolka},
title ={Proceedings of the 7th International Workshop on Verification of Infinite-State Systems (INFINITY'05)},
journal ={ENTCS},
volume ={149},
number ={1},
year ={2006},
ee ={http://dx.doi.org/10.1016/j.entcs.2005.11.012},
}