author ={J.S. Jensen and T.B. Kr{\o}gh and J.S. Madsen and S. Schmid and J. Srba and M.T. Thorgersen},

title ={P-Rex: Fast Verification of MPLS Networks with Multiple Link Failures},

booktitle ={Proceedings of the 14th International Conference on emerging Networking EXperiments and Technologies ({CoNEXT'18})},

year ={2018},

series ={},

volume ={},

pages ={1--13},

publisher ={},

abstract ={Future communication networks are expected to be highly automated, disburdening human operators of their most complex tasks. However, while first powerful and automated network analysis tools are emerging, existing tools provide very limited (and inefficient) support of reasoning about failure scenarios. We present P-Rex, a fast what-if analysis tool, that allows us to test important reachability and policy-compliance properties even under an arbitrary number of failures, in polynomial-time, i.e., without enumerating all failure scenarios (the usual approach today, if supported at all). P-Rex targets networks based on Multiprotocol Label Switching (MPLS) and its Segment Routing (SR) extension and comes with an expressive query language based on regular expressions. It takes into account the actual router tables, and is hence well-suited for debugging. We also report on an industrial case study and demonstrate that P-Rex supports rich queries, performing what-if analyses in less than 70 minutes in most cases, in a 24-router network with almost 1 million forwarding rules.},

note ={To appear.},

}

@inproceedings{ILSS:QEST:18,

author ={D. Ivanov and K.G. Larsen and S. Schupp and J. Srba},

title ={Analytical Solution for Long Battery Lifetime Prediction in Nonadaptive Systems},

booktitle ={Proceedings of the 15th International Conference on Quantitative Evaluation of SysTems ({QEST}'18)},

year ={2018},

series ={LNCS},

volume ={11024},

pages ={173--189},

publisher ={Springer-Verlag},

abstract ={Uppaal SMC is a state-of-the-art tool for modelling and statistical analysis of hybrid systems, allowing the user to directly model the expected battery consumption in battery-operated devices. The tool employs a numerical approach for solving differential equations describing the continuous evolution of a hybrid system, however, the addition of a battery model significantly slows down the simulation and decreases the precision of the analysis. Moreover, Uppaal SMC is not optimized for obtaining simulations with durations of realistic battery lifetimes. We propose an analytical approach to address the performance and precision issues of battery modelling, and a trace extrapolation technique for extending the prediction horizon of Uppaal SMC. Our approach shows a performance gain of up to 80% on two industrial wireless sensor protocol models, while improving the precision with up to 55%. As a proof of concept, we develop a tool prototype where we apply our extrapolation technique for predicting battery lifetimes and show that the expected battery lifetime for several months of device operation can be computed within a reasonable computation time.},

pdf ={http://www.cs.aau.dk/~srba/files/ILSS:QEST:18.pdf},

ee ={https://link.springer.com/chapter/10.1007%2F978-3-319-99154-2_11},

doi ={0.1007/978-3-319-99154-2_11},

isbn ={978-3-319-99153-5},

}

@inproceedings{BJLMS:CAV:18,

author ={F.M. Boenneland and P.G. Jensen and K.G. Larsen and M. Muniz and J. Srba},

title ={Start Pruning When Time Gets Urgent: Partial Order Reduction for Timed Systems},

booktitle ={Proceedings of the 30th International Conference on Computer Aided Verification ({CAV}'18)},

year ={2018},

series ={LNCS},

volume ={10981},

pages ={527--546},

publisher ={Springer-Verlag},

abstract ={Partial order reduction for timed systems is a challenging topic due to the dependencies among events induced by time acting as a global synchronization mechanism. So far, there has only been a limited success in finding practically applicable solutions yielding significant state space reductions. We suggest a working and efficient method to facilitate stubborn set reduction for timed systems with urgent behaviour. We first describe the framework in the general setting of timed labelled transition systems and then instantiate it to the case of timed-arc Petri nets. The basic idea is that we can employ classical untimed partial order reduction techniques as long as urgent behaviour is enforced. Our solution is implemented in the model checker TAPAAL and the feature is now broadly available to the users of the tool. By a series of larger case studies, we document the benefits of our method and its applicability to real-world scenarios.},

pdf ={http://www.cs.aau.dk/~srba/files/BJLMS:CAV:18.pdf},

ee ={https://link.springer.com/chapter/10.1007%2F978-3-319-96145-3_28},

doi ={10.1007/978-3-319-96145-3_28},

isbn ={978-3-319-96144-3},

}

@inproceedings{BDJJS:PN:18,

author ={F.M. Boenneland and J. Dyhr and P.G. Jensen and M. Johannsen and J. Srba},

title ={Simplification of CTL Formulae for Efficient Model Checking of Petri Nets},

booktitle ={Proceedings of the 39th International Conference on Application and Theory of {P}etri Nets and Concurrency ({Petri Nets}'18)},

year ={2018},

series ={LNCS},

volume ={10877},

pages ={143--163},

publisher ={Springer-Verlag},

abstract ={We study techniques to overcome the state space explosion problem in CTL model checking of Petri nets. Classical state space pruning approaches like partial order reductions and structural reductions become less efficient with the growing size of the CTL formula. The reason is that the more places and transitions are used as atomic propositions in a given formula, the more of the behaviour (interleaving) becomes relevant for the validity of the formula. We suggest several methods to reduce the size of CTL formulae, while preserving their validity. By these methods, we significantly increase the benefits of structural and partial order reductions, as the combination of our techniques can achive up to 60 percent average reduction in formulae sizes. The algorithms are implemented in the open-source verification tool TAPAAL and we document the efficiency of our approach on a large benchmark of Petri net models and queries from the Model Checking Contest 2017.},

pdf ={http://www.cs.aau.dk/~srba/files/BDJJS:PN:18.pdf},

ee ={https://link.springer.com/chapter/10.1007/978-3-319-91268-4_8},

doi ={10.1007/978-3-319-91268-4_8},

}

@inproceedings{INFOCOM:SS:18,

author ={S. Schmid and J. Srba},

title ={Polynomial-Time What-If Analysis for Prefix-Manipulating MPLS Networks},

booktitle ={{IEEE} International Conference on Computer Communications ({INFOCOM}'18)},

pages ={1--9},

year ={2018},

publisher ={{IEEE}},

note ={To appear.},

abstract ={While automated network verification is emerging as a critical enabler to manage large complex networks, current approaches come with a high computational complexity. This paper initiates the study of communication networks whose configurations can be verified fast, namely in polynomial time. In particular, we show that in communication networks based on prefix rewriting, which include MPLS networks, important network properties such as reachability, loop-freedom, and transparency, can be verified efficiently, even in the presence of failures. This enables a fast what-if analysis, addressing a major concern of network administrators: while configuring and testing network policies for a fully functional network is challenging, ensuring policy compliance in the face of (possibly multiple) failures, is almost impossible for human administrators. At the heart of our approach lies an interesting connection to the theory of prefix rewriting systems, a subfield of language and automata theory.},

pdf ={http://www.cs.aau.dk/~srba/files/INFOCOM:SS:18.pdf},

}

@inproceedings{JLS:ICTAC:17,

author ={P.G. Jensen and K.G. Larsen and J. Srba},

title ={{PT}rie: Data Structure for Compressing and Storing Sets via Prefix Sharing},

booktitle ={Proceedings of the 14th International Colloquium on Theoretical Aspects of Computing ({ICTAC}'17)},

year ={2017},

volume ={10580},

series ={LNCS},

pages ={248--265},

publisher ={Springer},

abstract ={Sets and their efficient implementation are fundamental in all of computer science, including model checking, where sets are used as the basic data structure for storing (encodings of) states during a state-space exploration. In the quest for fast and memory efficient methods for manipulating large sets, we present a novel data structure called PTrie for storing sets of binary strings of arbitrary length. The PTrie data structure distinguishes itself by compressing the stored elements while sharing the desirable key characteristics with conventional hash-based implementations, namely fast insertion and lookup operations. We provide the theoretical foundation of PTries, prove the correctness of their operations and conduct empirical studies analysing the performance of PTries for dealing with randomly generated binary strings as well as for state-space exploration of a large collection of Petri net models from the 2016 edition of the Model Checking Contest (MCC'16). We experimentally document that with a modest overhead in running time, a truly significant space-reduction can be achieved. Lastly, we provide an efficient implementation of the PTrie data structure under the GPL version 3 license, so that the technology is made available for memory-intensive applications such as model-checking tools.},

pdf ={http://www.cs.aau.dk/~srba/files/JLS:ICTAC:17.pdf},

ee ={https://link.springer.com/chapter/10.1007/978-3-319-67729-3_15},

doi ={10.1007/978-3-319-67729-3_15},

}

@inproceedings{DEFJJKLNOPS:PN:2017,

author ={A.E. Dalsgaard and S. Enevoldsen and P. Fogh and L.S. Jensen and T.S. Jepsen and I. Kaufmann and K.G. Larsen and S.M. Nielsen and M.Chr. Olesen and S. Pastva and J. Srba},

title ={Extended Dependency Graphs and Efficient Distributed Fixed-Point Computation},

booktitle ={Proceedings of the 38th International Conference on Application and Theory of {P}etri Nets and Concurrency ({Petri Nets}'17)},

year ={2017},

series ={LNCS},

volume ={10258},

pages ={139--158},

publisher ={Springer-Verlag},

abstract ={Equivalence and model checking problems can be encoded into computing fixed points on dependency graphs. Dependency graphs represent causal dependencies among the nodes of the graph by means of hyper-edges. We suggest to extend the model of dependency graphs with so-called negation edges in order to increase their applicability. The graphs (as well as the verification problems) suffer from the state space explosion problem. To combat this issue, we design an on-the-fly algorithm for efficiently computing fixed points on extended dependency graphs. Our algorithm supplements previous approaches with the possibility to back-propagate, in certain scenarios, the domain value 0, in addition to the standard back-propagation of the value 1. Finally, we design a distributed version of the algorithm, implement it in an open-source tool, and demonstrate the efficiency of our general approach on the benchmark of Petri net models and CTL queries from the Model Checking Contest 2016.},

pdf ={http://www.cs.aau.dk/~srba/files/DEFJJKLNOPS:PN:2017.pdf},

doi ={10.1007/978-3-319-57861-3_10},

ee ={http://link.springer.com/chapter/10.1007/978-3-319-57861-3_10},

}

@inproceedings{DELS:SETTA:16,

author ={A.E. Dalsgaard and S. Enevoldsen and K.G. Larsen and J. Srba},

title ={Distributed Computation of Fixed Points on Dependency Graphs},

booktitle ={Proceedings of Symposium on Dependable Software Engineering: Theories, Tools and Applications ({SETTA}'16)},

year ={2016},

pages ={197--212},

publisher ={Springer},

series ={LNCS},

volume ={9984},

abstract ={Dependency graph is an abstract mathematical structure for representing complex causal dependencies among its vertices. Several equivalence and model checking questions, boolean equation systems and other problems can be reduced to fixed-point computations on dependency graphs. We develop a novel distributed algorithm for computing such fixed points, prove its correctness and provide an efficient, open-source implementation of the algorithm. The algorithm works in an on-the-fly manner, eliminating the need to generate a priori the entire dependency graph. We evaluate the applicability of our approach by a number of experiments that verify weak simulation/bisimulation equivalences between CCS processes and we compare the performance with the well-known CWB tool. Even though the fixed-point computation, being a P-complete problem, is difficult to parallelize in theory, we achieve significant speed-ups in the performance as demonstrated on a Linux cluster with several hundreds of cores.},

pdf ={http://www.cs.aau.dk/~srba/files/DELS:SETTA:16.pdf},

doi ={10.1007/978-3-319-47677-3_13},

ee ={http://link.springer.com/chapter/10.1007/978-3-319-47677-3_13},

}

@inproceedings{ALMMOPSS:IECON:16,

author ={M.K. Agesen and K.G. Larsen and M. Mikucionis and M. Muniz and P. Olsen and T. Pedersen and J. Srba and A. Skou},

title ={Toolchain for User-Centered Intelligent Floor Heating Control},

booktitle ={Proceedings of the 42nd Annual Conference of the IEEE Industrial Electronics Society ({IECON'16})},

year ={2016},

pages ={5296--5301},

publisher ={IEEE},

abstract ={Floor heating systems are important components of nowadays home-automation setups. The control of a floor heating system is a nontrivial task and the present solutions essentially implement variants of a simple bang-bang controller that opens for a hot water circulation in a room if its current temperature is below the user defined target temperature, otherwise it closes for the heating in the room. The disadvantage is that the heat exchange among the rooms, outside weather conditions, weather forecast and other factors are not considered. We propose a novel model-driven approach for intelligent floor heating control based on a chain of tools that allow us to gather the sensor readings from the actual hardware and use the state-of-the-art controller synthesis tool UPPAAL Stratego in order to synthesise abstract control strategies that are then executed on the real hardware platform provided by the company Seluxit. We have built a scaled demonstrator of the system and the experimental results document a 38% to 52% increase in user satisfaction, moreover with additional energy savings between 2% to 12%.},

pdf ={http://www.cs.aau.dk/~srba/files/ALMMOPSS:IECON:16.pdf},

doi ={10.1109/IECON.2016.7794040},

ee ={http://ieeexplore.ieee.org/document/7794040/},

}

@inproceedings{JLS:SPIN:16,

author ={P.G. Jensen and K.G. Larsen and J. Srba},

title ={Real-Time Strategy Synthesis for Timed-Arc {P}etri Net Games via Discretization},

booktitle ={Proceedings of the 23rd International SPIN Symposium on Model Checking of Software ({SPIN}'16)},

year ={2016},

series ={LNCS},

volume ={9641},

pages ={129--146},

publisher ={Springer-Verlag},

abstract ={Automatic strategy synthesis for a given control objective can be used to generate correct-by-construction controllers of reactive systems. The existing symbolic approach for continuous timed games is a computationally hard task and current tools like UPPAAL TiGa often scale poorly with the model complexity. We suggest an explicit approach for strategy synthesis in the discrete-time setting and show that even for systems with closed guards, the existence of a safety discrete-time strategy does not imply the existence of a safety continuous-time strategy and vice versa. Nevertheless, we prove that the answers to the existence of discrete-time and continuous-time safety strategies coincide on a practically motivated subclass of urgent controllers that either react immediately after receiving an environmental input or wait with the decision until a next event is triggered by the environment. We then develop an on-the-fly synthesis algorithm for discrete timed-arc Petri net games. The algorithm is implemented in our tool TAPAAL and based on the experimental evidence, we discuss the advantages of our approach compared to the symbolic continuous-time techniques.},

pdf ={http://www.cs.aau.dk/~srba/files/JLS:SPIN:16.pdf},

doi ={10.1007/978-3-319-32582-8_9},

ee ={http://link.springer.com/chapter/10.1007%2F978-3-319-32582-8_9},

}

@inproceedings{LMMST:TACAS:16,

author ={K.G. Larsen and M. Mikucionis and M. Muniz and J. Srba and J.H. Taankvist},

title ={Online and Compositional Learning of Controllers with Application to Floor Heating},

booktitle ={Proceedings of the 22nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems ({TACAS}'16)},

year ={2016},

series ={LNCS},

volume ={9636},

publisher ={Springer-Verlag},

pages ={244--259},

abstract ={Controller synthesis for stochastic hybrid switched systems, like e.g. a floor heating system in a house, is a complex computational task that cannot be solved by an exhaustive search though all the control options. The state-space to be explored is in general uncountable due to the presence of continuous variables (e.g. temperature readings in the different rooms) and even after digitization, the state-space remains huge and cannot be fully explored. We suggest a general and scalable methodology for controller synthesis for such systems. Instead of off-line synthesis of a controller for all possible input temperatures and an arbitrary time horizon, we propose an on-line synthesis methodology, where we periodically compute the controller only for the near future based on the current sensor readings. This computation is itself done by employing machine learning in order to avoid enumeration of the whole state-space. For additional scalability we propose and apply a compositional synthesis approach. Finally, we demonstrate the applicability of the methodology to a concrete floor heating system of a real family house.},

pdf ={http://www.cs.aau.dk/~srba/files/LMMST:TACAS:16.pdf},

doi ={10.1007/978-3-662-49674-9_14},

ee ={http://link.springer.com/chapter/10.1007%2F978-3-662-49674-9_14},

}

@inproceedings{AAEHLOSW:ICTAC:15,

author ={J.R. Andersen and N. Andersen and S. Enevoldsen and M.M. Hansen and K.G. Larsen and S.R. Olesen and J. Srba and J.K. Wortmann},

title ={{CAAL}: Concurrency Workbench, {A}alborg Edition},

booktitle ={Proceedings of the 12th International Colloquium on Theoretical Aspects of Computing ({ICTAC}'15)},

year ={2015},

volume ={9399},

series ={LNCS},

pages ={573--582},

publisher ={Springer},

abstract ={We present the first official release of CAAL, a web-based tool for modelling and verification of concurrent processes. The tool is primarily designed for educational purposes and it supports the classical process algebra CCS together with its timed extension TCCS. It allows to compare processes with respect to a range of strong/weak and timed/untimed equivalences and preorders (bisimulation, simulation and traces) and supports model checking of CCS/TCCS processes against recursively defined formulae of Hennessy-Milner logic. The tool offers a graphical visualizer for displaying labelled transition systems, including their minimization up to strong/weak bisimulation, and process behaviour can be examined by playing (bi)simulation and model checking games or via the generation of distinguishing formulae for non-equivalent processes. We describe the modelling and analysis features of CAAL, discuss the underlying verification algorithms and show a typical example of a use in the classroom environment.},

pdf ={http://www.cs.aau.dk/~srba/files/AAEHLOSW:ICTAC:15.pdf},

ee ={http://link.springer.com/chapter/10.1007%2F978-3-319-25150-9_33},

doi ={10.1007/978-3-319-25150-9_33},

}

@inproceedings{KLLS:CONCUR:15,

author ={J. K\v{r}et\'{\i}nsk\'{y} and K.G. Larsen and S. Laursen and J. Srba},

title ={Polynomial Time Decidability of Weighted Synchronization under Partial Observability},

booktitle ={Proceedings of the 26th International Conference on Concurrency Theory ({CONCUR}'15)},

year ={2015},

volume ={42},

series ={LIPICS},

pages ={142--154},

publisher ={Dagstuhl Publishing},

abstract ={We consider weighted automata with both positive and negative integer weights on edges and study the problem of synchronization using adaptive strategies that may only observe whether the current weight-level is negative or nonnegative. We show that the synchronization problem is decidable in polynomial time for deterministic weighted automata. },

pdf ={http://www.cs.aau.dk/~srba/files/KLLS:CONCUR:15.pdf},

ee ={http://dx.doi.org/10.4230/LIPIcs.CONCUR.2015.142},

doi ={10.4230/LIPIcs.CONCUR.2015.142},

}

@inproceedings{BBLS:ICALP:15,

author ={N. Bene\v{s} and P. Bezdek and K.G. Larsen and J. Srba},

title ={Language Emptiness of Continuous-Time Parametric Timed Automata},

booktitle ={Proceedings of the 42nd International Colloquium on Automata, Languages and Programming ({ICALP}'15)},

year ={2015},

series ={LNCS},

volume ={9135},

pages ={69--81},

publisher ={Springer-Verlag},

abstract ={Parametric timed automata extend the standard timed automata with the possibility to use parameters in the clock guards. In general, if the parameters are real-valued, the problem of language emptiness of such automata is undecidable even for various restricted subclasses. We thus focus on the case where parameters are assumed to be integer-valued, while the time still remains continuous. On the one hand, we show that the problem remains undecidable for parametric timed automata with three clocks and one parameter. On the other hand, for the case with arbitrary many clocks where only one of these clocks is compared with (an arbitrary number of) parameters, we show that the parametric language emptiness is decidable. The undecidability result tightens the bounds of a previous result which assumed six parameters, while the decidability result extends the existing approaches that deal with discrete-time semantics only. To the best of our knowledge, this is the first positive result in the case of continuous-time and unbounded integer parameters, except for the rather simple case of single-clock automata.},

pdf ={http://www.cs.aau.dk/~srba/files/BBLS:ICALP:15.pdf},

doi ={10.1007/978-3-662-47666-6},

ee ={http://link.springer.com/chapter/10.1007%2F978-3-662-47666-6_6},

}

@inproceedings{BJJMSS:FORMATS:14,

author ={S.V. Birch and T.S. Jacobsen and J.J. Jensen and Ch. Moesgaard and N.N. Samuelsen and J. Srba},

title ={Interval Abstraction Refinement for Model Checking of Timed-Arc {P}etri Nets},

booktitle ={Proceedings of the 12th International Conference on Formal Modelling and Analysis of Timed Systems (FORMATS'14)},

year ={2014},

series ={LNCS},

volume ={8711},

pages ={237--251},

publisher ={Springer-Verlag},

abstract ={ State-space explosion is a major obstacle in verification of time-critical distributed systems. An important factor with a negative influence on the tractability of the analysis is the size of constants that clocks are compared to. This problem is particularly accented in explicit state-space exploration techniques. We suggest an approximation method for reducing the size of constants present in the model. The proposed method is developed for Timed-Arc Petri Nets and creates an under-approximation or an over-approximation of the model behaviour. The verification of approximated Petri net models can be considerably faster but it does not in general guarantee conclusive answers. We implement the algorithms within the open-source model checker TAPAAL and demonstrate on a number of experiments that our approximation techniques often result in a significant speed-up of the verification.},

pdf ={http://www.cs.aau.dk/~srba/files/BJJMSS:FORMATS:14.pdf},

ee ={http://link.springer.com/chapter/10.1007%2F978-3-319-10512-3_17},

doi ={10.1007/978-3-319-10512-3_17},

}

@inproceedings{LLS:CONCUR:14,

author ={K.G. Larsen and S. Laursen and J. Srba},

title ={Synchronizing Strategies under Partial Observability},

booktitle ={Proceedings of the 25th International Conference on Concurrency Theory (CONCUR'14)},

year ={2014},

volume ={8704},

series ={LNCS},

pages ={188--202},

publisher ={Springer-Verlag},

abstract ={Embedded devices usually share only partial information about their current configurations as the communication bandwidth can be restricted. Despite this, we may wish to bring a failed device into a given predetermined configuration. This problem, also known as resetting or synchronizing words, has been intensively studied for systems that do not provide any information about their configurations. In order to capture more general scenarios, we extend the existing theory of synchronizing words to synchronizing strategies, and study the synchronization, short-synchronization and subset-to-subset synchronization problems under partial observability. We provide a comprehensive complexity analysis of these problems, concluding that for deterministic systems the complexity of the problems under partial observability remains the same as for the classical synchronization problems, whereas for nondeterministic systems the complexity increases already for systems with just two observations, as we can now encode alternation.},

pdf ={http://www.cs.aau.dk/~srba/files/LLS:CONCUR:14.pdf},

ee ={http://link.springer.com/chapter/10.1007/978-3-662-44584-6_14},

doi ={10.1007/978-3-662-44584-6_14},

}

@inproceedings{MSS:PN:14,

author ={J.A. Mateo and J. Srba and M.G. S{\o}rensen},

title ={Soundness of Timed-Arc Workflow Nets},

booktitle ={Proceedings of the 35th International Conference on Application and Theory of {P}etri Nets and Concurrency ({ICATPN}'14)},

year ={2014},

series ={LNCS},

volume ={8489},

pages ={51--70},

publisher ={Springer-Verlag},

abstract ={Analysis of workflow processes with quantitative aspects like timing is of interest in numerous time-critical applications. We suggest a workflow model based on timed-arc Petri nets and study the foundational problems of soundness and strong (time-bounded) soundness. We explore the decidability of these problems and show, among others, that soundness is decidable for monotonic workflow nets while reachability is undecidable. For general timed-arc workflow nets soundness and strong soundness become undecidable, though we can design efficient verification algorithms for the subclass of bounded nets. Finally, we demonstrate the usability of our theory on the case studies of a Brake System Control Unit used in aircraft certification, the MPEG2 encoding algorithm, and a blood transfusion workflow. The implementation of the algorithms is freely available as a part of the model checker TAPAAL.},

pdf ={http://www.cs.aau.dk/~srba/files/MSS:PN:14.pdf},

ee ={http://link.springer.com/chapter/10.1007/978-3-319-07734-5_4},

doi ={10.1007/978-3-319-07734-5_4},

}

@inproceedings{JLSST:NFM:14,

author ={P.G. Jensen and K.G. Larsen and J. Srba and M.G. S{\o}rensen and J.H. Taankvist},

title ={Memory Efficient Data Structures for Explicit Verification of Timed Systems},

booktitle ={Proceedings of the 6th NASA Formal Methods Symposium ({NFM}'14)},

year ={2014},

series ={LNCS},

volume ={8430},

pages ={307--312},

publisher ={Springer-Verlag},

abstract ={Timed analysis of real-time systems can be performed usingcontinuous (symbolic) or discrete (explicit) techniques. The explicit state-space exploration can be considerably fasterfor models with moderately small constants, however,at the expense of high memory consumption. In the setting of timed-arc Petri nets, we explore new data structures for loweringthe used memory: PTries for efficient storing of configurationsand time darts for semi-symbolic description of the state-space. Both methods are implemented as a part of the tool TAPAAL and the experiments document at least one order of magnitude of memory savings while preserving comparable verification times.},

pdf ={http://www.cs.aau.dk/~srba/files/JLSST:NFM:14.pdf},

ee ={http://link.springer.com/chapter/10.1007/978-3-319-06200-6_26},

doi ={10.1007/978-3-319-06200-6_26},

}

@inproceedings{JLSO:SPIN:13,

author ={J.F. Jensen and K.G. Larsen and J. Srba and L.K. Oestergaard},

title ={Local Model Checking of Weighted {CTL} with Upper-Bound Constraints},

booktitle ={Proceedings of International SPIN Symposium on Model Checking of Software ({SPIN}'13)},

year ={2013},

series ={LNCS},

volume ={7976},

pages ={178--195},

publisher ={Springer-Verlag},

abstract ={We present a symbolic extension of dependency graphs by Liu and Smolka in order to model-check weighted Kripke structures against the logic CTL with upper-bound weight constraints. Our extension introduces a new type of edges into dependency graphs and lifts the computation of fixed-points from boolean domain to nonnegative integers in order to cope with the weights. We present both global and local algorithms for the fixed-point computation on symbolic dependency graphs and argue for the advantages of our approach compared to the direct encoding of the model checking problem into dependency graphs. We implement all algorithms in a publicly available tool prototype and evaluate them on several experiments. The principal conclusion is that our local algorithm is the most efficient one with an order of magnitude improvement for model checking problems with a high number of `witnesses'.},

pdf ={http://www.cs.aau.dk/~srba/files/JLSO:SPIN:13.pdf},

ee ={http://dx.doi.org/10.1007/978-3-642-39176-7_12},

doi ={10.1007/978-3-642-39176-7_12},

}

@inproceedings{ALSST:MEMICS:12,

author ={M. Andersen and H.G. Larsen and J. Srba and M.G. S{\o}rensen and J.H. Taankvist},

title ={Verification of Liveness Properties on Closed Timed-Arc Petri Nets},

booktitle ={Proceedings of the 8th Annual Doctoral Workshop on Mathematical and Engineering Methods in Computer Science ({MEMICS}'12)},

year ={2013},

series ={LNCS},

publisher ={Springer-Verlag},

volume ={7721},

pages ={69--81},

abstract ={Verification of closed timed models by explicit state-spaceexploration methods is an alternative to the wide-spread symbolic techniquesbased on difference bound matrices (DBMs). A few experiments found in theliterature confirm that for the reachability analysis of timed automataexplicit techniques can compete with DBM-based algorithms, at least forsituations where the constants used in the models are relatively small.To the best of our knowledge, the explicit methods have not yet beenemployed in the verification of liveness properties in Petri net modelsextended with time. We present an algorithm for liveness analysis of closedTimed-Arc Petri Nets (TAPN) extended with weights, transport arcs,inhibitor arcs and age invariants and prove its correctness. The algorithmcomputes optimized maximum constants for each place in the net that boundthe size of the reachable state-space. We document the efficiency of thealgorithm by experiments comparing its performance with the state-of-the-artmodel checker UPPAAL.},

pdf ={http://www.cs.aau.dk/~srba/files/ALSST:MEMICS:12.pdf},

ee ={http://dx.doi.org/10.1007/978-3-642-36046-6_8},

doi ={10.1007/978-3-642-36046-6_8},

}

@inproceedings{LLS:MEMICS:12,

author ={K.G. Larsen and S. Laursen and J. Srba},

title ={Action Investment Energy Games},

booktitle ={Proceedings of the 8th Annual Doctoral Workshop on Mathematical and Engineering Methods in Computer Science ({MEMICS}'12)},

year ={2013},

series ={LNCS},

publisher ={Springer-Verlag},

volume ={7721},

pages ={155--167},

abstract ={We introduce the formalism of action investment energy gameswhere we study the trade-off between investments limited by given budgets andresource constrained (energy) behavior of the underlying system. Morespecifically, we consider energy games extended with costs of enabling actionsand fixed budgets for each player. We ask the question whether for any Player2 investment there exists a Player 1 investment such that Player 1 wins theresulting energy game. We study the action investment energy game for energyintervals with both upper and lower bounds, and with a lower bound only, andgive a complexity results overview for the problem of deciding thewinner in the game.},

pdf ={http://www.cs.aau.dk/~srba/files/LLS:MEMICS:12.pdf},

ee ={http://dx.doi.org/10.1007/978-3-642-36046-6_15},

doi ={10.1007/978-3-642-36046-6_15},

}

@inproceedings{BLS:FHIES:12,

author ={C. Bertolini and Zh. Liu and J. Srba},

title ={Verification of Timed Healthcare Workflows Using Component Timed-Arc Petri Nets},

booktitle ={Proceedings of the 2nd International Symposium on the Foundations of Health Information Engineering and Systems ({FHIES}'12)},

year ={2013},

publisher ={Springer-Verlag},

volume ={7789},

pages ={19--36},

series ={LNCS},

abstract ={Workflows in modern healthcare systems are becoming increasinglycomplex and their execution involves concurrency and sharing of resources.The definition, analysis and management of collaborative healthcare workflowsrequires abstract model notations with a precisely defined semantics and asupport for compositional reasoning. We use the formalism of component-basedtimed-arc Petri Nets (CTAPN) for modular modelling of collaborative healthcareworkflows and demonstrate how the model checker TAPAAL supports theverification of their functional and non-functional requirements.To this end, we use CTAPN to define the semantics of the healthcaredomain specific graphical notation Little-JIL, extended with timingconstrains, and apply it to the case study of blood transfusion. Thevalue added in general, and to Little-JIL in particular, is the formalsupport for compositional modelling, analysis and verification,including an explicit treatment of the timing aspects.},

pdf ={http://www.cs.aau.dk/~srba/files/BLS:FHIES:12.pdf},

doi ={10.1007/978-3-642-39088-3_2},

ee ={http://dx.doi.org/10.1007/978-3-642-39088-3_2},

}

@inproceedings{DJJS:SSV:12,

author ={A. David and L. Jacobsen and M. Jacobsen and J. Srba},

title ={A Forward Reachability Algorithm for Bounded Timed-Arc {P}etri Nets},

booktitle ={Proceedings of the 7th International Conference on Systems Software Verification ({SSV}'12)},

year ={2012},

series ={EPTCS},

volume ={102},

pages ={125-140},

publisher ={Open Publishing Association},

abstract ={Timed-arc Petri nets (TAPN) are a well-known time extension of thePetri net model and several translations to networks of timedautomata have been proposed for this model.We present a direct, DBM-basedalgorithm for forward reachability analysis of bounded TAPNs extended with transport arcs, inhibitor arcs and age invariants.We also give a complete proof of its correctness,including reduction techniques based on symmetries and extrapolation.Finally, we augment the algorithm with a novel state-spacereduction technique introducing a monotonic ordering on markings and prove its soundness even in the presence of monotonicity-breaking features like age invariants and inhibitor arcs. We implement the algorithm within the model-checkerTAPAAL and the experimental results document an encouraging performance compared to verification approaches that translate TAPN models to UPPAAL timed automata.},

pdf ={http://www.cs.aau.dk/~srba/files/DJJS:SSV:12.pdf},

doi ={10.4204/EPTCS.102.12},

ee ={http://dx.doi.org/10.4204/EPTCS.102.12},

}

@inproceedings{JLS:SSV:12,

author ={K.Y. J{\o}rgensen and K.G. Larsen and J. Srba},

title ={Time-Darts: A Data Structure for Verification of Closed Timed Automata},

booktitle ={Proceedings of the 7th International Conference on Systems Software Verification ({SSV}'12)},

year ={2012},

series ={EPTCS},

volume ={102},

pages ={141-155},

publisher ={Open Publishing Association},

abstract ={Symbolic data structures for model checking timed systems have been subject to a significant research, with Difference Bound Matrices (DBMs) still being the preferred data structure in several mature verification tools. In comparison, discretization offers an easy alternative, with all operations having linear-time complexity in the number of clocks, and yet valid for a large class of closed systems. Unfortunately, fine-grained discretization causes itself a state-space explosion. We introduce a new data structure called time-darts for the symbolic representation of state-spaces of timed automata. Compared with the complete discretization, a single time-dart allows to represent an arbitrary large set of states, yet the time complexity of operations on time-darts remain linear in the number of clocks. We prove the correctness of the suggested reachability algorithm and perform several experiments in order to compare the performance of time-darts and the complete discretization. The main conclusion is that in all our experiments the time-dart method outperforms the complete discretization and it scales significantly better for models with larger constants.},

pdf ={http://www.cs.aau.dk/~srba/files/JLS:SSV:12.pdf},

doi ={10.4204/EPTCS.102.13},

ee ={http://dx.doi.org/10.4204/EPTCS.102.13},

}

@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},

pages ={103--108},

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.},

pdf ={http://www.cs.aau.dk/~srba/files/DFLSZZ:CBSE:12.pdf},

ee ={http://dx.doi.org/10.1145/2304736.2304754},

}

@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},

pages ={77--84},

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.},

ee ={http://doi.ieeecomputersociety.org/10.1109/TASE.2012.9},

pdf ={http://www.cs.aau.dk/~srba/files/BJLLS:TASE:12.pdf},

isbn ={978-0-7695-4751-0},

}

@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.cs.aau.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.cs.aau.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.cs.aau.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.cs.aau.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.cs.aau.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.cs.aau.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.cs.aau.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.cs.aau.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.cs.aau.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.cs.aau.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.cs.aau.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.cs.aau.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.cs.aau.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.cs.aau.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.cs.aau.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.cs.aau.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.cs.aau.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.cs.aau.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.cs.aau.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.cs.aau.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.cs.aau.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.cs.aau.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.cs.aau.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.cs.aau.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.cs.aau.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.cs.aau.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.cs.aau.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.cs.aau.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 Language 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.cs.aau.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.cs.aau.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.cs.aau.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.cs.aau.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.cs.aau.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.cs.aau.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.cs.aau.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.cs.aau.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.cs.aau.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.cs.aau.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.cs.aau.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.cs.aau.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.cs.aau.dk/~srba/roadmap},

}

@article{BDJJS:JLAMP:18,

author ={F. B{\o}nneland and J. Dyhr and P.G. Jensen and M. Johannsen and J. Srba},

title ={Stubborn Versus Structural Reductions for Petri Nets},

journal ={Journal of Logical and Algebraic Methods in Programming},

year ={2018},

volume ={},

number ={},

pages ={1--29},

publisher ={Elsevier},

abstract ={Partial order and structural reduction techniques are some of the most beneficial methods for state space reduction in reachability analysis of Petri nets. This is among others documented by the fact that these techniques are used by the leading tools in the annual Model Checking Contest (MCC) of Petri net tools. We suggest improved versions of a partial order reduction based on stubborn sets and of a structural reduction with additional new reduction rules, and we extend both methods for the application on Petri nets with weighted arcs and weighted inhibitor arcs. All algorithms are implemented in the open-source verification tool TAPAAL and evaluated on a large benchmark of Petri net models from MCC'17, including a comparison with the tool LoLA (the last year winner of the competition). The experiments document that both methods provide significant state space reductions and, even more importantly, that their combination is indeed beneficial as a further nontrivial state space reduction can be achieved.},

note ={To appear.},

}

@article{DEFJJJKLNOPS:FI:18,

author ={A.E. Dalsgaard and S. Enevoldsen and P. Fogh and L.S. Jensen and P.G. Jensen and T.S. Jepsen and I. Kaufmann and K.G. Larsen and S.M. Nielsen and M.Chr. Olesen and S. Pastva and J. Srba},

title ={A Distributed Fixed-Point Algorithm for Extended Dependency Graphs},

journal ={Fundamenta Informaticae},

year ={2018},

volume ={161},

number ={4},

pages ={351--381},

publisher ={IOS Press},

abstract ={Equivalence and model checking problems can be encoded into computing fixed points on dependency graphs. Dependency graphs represent causal dependencies among the nodes of the graph by means of hyper-edges. We suggest to extend the model of dependency graphs with so-called negation edges in order to increase their applicability. The graphs (as well as the verification problems) suffer from the state space explosion problem. To combat this issue, we design an on-the-fly algorithm for efficiently computing fixed points on extended dependency graphs. Our algorithm supplements previous approaches with the possibility to back-propagate, in certain scenarios, the domain value 0, in addition to the standard back-propagation of the value 1. Finally, we design a distributed version of the algorithm, implement it in our open-source tool TAPAAL, and demonstrate the efficiency of our general approach on the benchmark of Petri net models and CTL queries from the annual Model Checking Contest.},

pdf ={http://www.cs.aau.dk/~srba/files/DEFJJJKLNOPS:FI:18.pdf},

issn ={0169-2968},

doi ={10.3233/FI-2018-1707},

ee ={https://content.iospress.com/articles/fundamenta-informaticae/fi1707},

}

@article{JLS:STTT:17,

author ={P.G. Jensen and K.G. Larsen and J. Srba},

title ={Discrete and Continuous Strategies for Timed-Arc {P}etri Net Games},

journal ={International Journal on Software Tools for Technology Transfer (STTT)},

year ={2018},

volume ={20},

number ={5},

publisher ={Springer-Verlag},

pages ={529--546},

abstract ={Automatic strategy synthesis for a given control objective can be used to generate correct-by-construction controllers of real-time reactive systems. The existing symbolic approach for continuous timed games is a computationally hard task and current tools like UPPAAL TiGa often scale poorly with the model complexity. We suggest an explicit approach for strategy synthesis in the discrete-time setting and show that even for systems with closed guards, the existence of a safety discrete-time strategy does not imply the existence of a safety continuous-time strategy and vice versa. Nevertheless, we prove that the answers to the existence of discrete-time and continuous-time safety strategies coincide on a practically motivated subclass of urgent controllers that either react immediately after receiving an environmental input or wait with the decision until a next event is triggered by the environment. We then develop an on-the-fly synthesis algorithm for discrete timed-arc Petri net games. The algorithm is implemented in our tool TAPAAL and based on the experimental evidence, we discuss the advantages of our approach compared to the symbolic continuous-time techniques.},

pdf ={http://www.cs.aau.dk/~srba/files/JLS:STTT:17.pdf},

issn ={1433-2779},

doi ={10.1007/s10009-017-0473-2},

ee ={https://link.springer.com/article/10.1007%2Fs10009-017-0473-2},

}

@article{JNOS:ToPNoC:16,

author ={J.F. Jensen and T. Nielsen and L.K. Oestergaard and J. Srba},

title ={TAPAAL and Reachability Analysis of P/T Nets},

journal ={LNCS Transactions on Petri Nets and Other Models of Concurrency (ToPNoC)},

year ={2016},

publisher ={Springer-Verlag},

series ={LNCS},

volume ={9930},

pages ={307--318},

abstract ={We discuss selected model checking techniques used in the tool TAPAAL for the reachability analysis of weighted Petri nets with inhibitor arcs. We focus on techniques that had the most significant effect at the 2015 Model Checking Contest (MCC). While the techniques are mostly well known, our contribution lies in their adaptation to the MCC reachability queries, their efficient implementation and the evaluation of their performance on a large variety of nets from MCC'15.},

pdf ={http://www.cs.aau.dk/~srba/files/JNOS:ToPNoC:16.pdf},

issn ={0302-9743},

doi ={10.1007/978-3-662-53401-4_16},

ee ={http://link.springer.com/chapter/10.1007%2F978-3-662-53401-4_16},

}

@article{JLSO:STTT:14,

author ={J.F. Jensen and K.G. Larsen and J. Srba and L.K. Oestergaard},

title ={Efficient Model Checking of Weighted {CTL} with Upper-Bound Constraints},

journal ={International Journal on Software Tools for Technology Transfer (STTT)},

year ={2016},

volume ={18},

number ={4},

publisher ={Springer-Verlag},

pages ={409--426},

abstract ={We present a symbolic extension of dependency graphs by Liuand Smolka in order to model-check weighted Kripke structures againstthe logic CTL with upper-bound weight constraints. Our extension introducesa new type of edges into dependency graphs and lifts the computation offixed-points from boolean domain to nonnegative integers in order to copewith the weights. We present both global and local algorithms for thefixed-point computation on symbolic dependency graphs and argue for theadvantages of our approach compared to the direct encoding of the modelchecking problem into dependency graphs. We implement all algorithmsin a publicly available tool prototype and evaluate them on severalexperiments. The principal conclusion is that our local algorithm isthe most efficient one with an order of magnitude improvement formodel checking problems with a high number of `witnesses'.},

pdf ={http://www.cs.aau.dk/~srba/files/JLSO:STTT:14.pdf},

issn ={1433-2779},

doi ={10.1007/s10009-014-0359-5},

ee ={http://link.springer.com/article/10.1007%2Fs10009-014-0359-5},

}

@article{MSS:FI:15,

author ={J.A. Mateo and J. Srba and M.G. S{\o}rensen},

title ={Soundness of Timed-Arc Workflow Nets in Discrete and Continuous-Time Semantics},

journal ={Fundamenta Informaticae},

year ={2015},

volume ={140},

number ={1},

pages ={89--121},

publisher ={IOS Press},

abstract ={Analysis of workflow processes with quantitative aspectslike timing is of interest in numerous time-critical applications. We suggest a workflow model based on timed-arc Petri nets and studythe foundational problems of soundness and strong (time-bounded) soundness.We first consider the discrete-time semantics (integer delays)and explore the decidability of the soundness problemsand show, among others, that soundness is decidable for monotonic workflow nets while reachability is undecidable.For general timed-arc workflow nets soundness andstrong soundness become undecidable, though we can design efficientverification algorithms for the subclass of bounded nets. We also discuss the soundness problem in the continuous-timesemantics (real-number delays) and show that for nets withnonstrict guards (where the reachability question coincides for bothsemantics) the soundness checking problem does not in generalfollow the approach for the discrete semantics and different zone-basedtechniques are needed for introducing its decidability in the bounded case.Finally, we demonstrate the usability of our theory onthe case studies of a Brake System Control Unit used in aircraft certification, the MPEG2 encoding algorithm, and a blood transfusion workflow.The implementation of the algorithms is freely available as a part of the model checker TAPAAL (www.tapaal.net).},

pdf ={http://www.cs.aau.dk/~srba/files/MSS:FI:15.pdf},

doi ={10.3233/FI-2015-1246},

ee ={http://dx.doi.org/10.3233/FI-2015-1246},

}

@article{BKLMSS:AI:15,

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 S. Sickert and J. Srba},

title ={Refinement Checking on Parametric Modal Transition Systems},

journal ={Acta Informatica},

year ={2015},

volume ={52},

number ={2--3},

pages ={269--297},

publisher ={Springer-Verlag},

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 overcomes many of the limitations. We investigate the computational complexity of modal and thorough refinement checking on PMTS and its subclasses and provide a direct encoding of the modal refinement problem into quantified Boolean formulae, allowing us to employ state-of-the-art QBF solvers for modal refinement checking. The experiments we report on show that the feasibility of refinement checking is more influenced by the degree of nondeterminism rather than by the syntactic restrictions on the types of formulae allowed in the description of the PMTS.},

pdf ={http://www.cs.aau.dk/~srba/files/BKLMSS:AI:15.pdf},

doi ={10.1007/s00236-015-0215-4},

ee ={http://link.springer.com/article/10.1007%2Fs00236-015-0215-4},

}

@article{BJJJMS:TCS:13,

author ={J. Byg and M. Jacobsen and L. Jacobsen and K.Y. J{\o}rgensen and M.H. M{\o}ller and J. Srba},

title ={TCTL-Preserving Translations from Timed-Arc {P}etri Nets to Networks of Timed Automata},

journal ={Theoretical Computer Science },

publisher ={Elsevier},

volume ={537},

number ={5},

year ={2014},

pages ={3--28},

issn ={0304-3975},

doi ={10.1016/j.tcs.2013.07.011},

abstract ={We present a framework for TCTL-preserving translations between time-dependent modelling formalisms. The framework guarantees that once the original and the translated system are in one-by-many correspondence relation (a notion of behavioural equivalence between timed transition systems) then TCTL properties of the original system can be transformed too while preserving the verification answers. We demonstrate the usability of the technique on two reductions from bounded timed-arc Petri nets to networks for timed automata, providing unified proofs of the translations implemented in the verification tool TAPAAL. We evaluate the efficiency of the approach on a number of experiments: alternating bit protocol, Fischerʼs protocol, Lynch-Shavit protocol, MPEG-2 encoder, engine workshop and medical workflow. The results are encouraging and confirm the practical applicability of the approach.},

ee ={http://dx.doi.org/10.1016/j.tcs.2013.07.011},

pdf ={http://www.cs.aau.dk/~srba/files/BJJJMS:TCS:13.pdf},

}

@article{MRSV:STTT:13,

title ={Model-Checking Web Services Business Activity Protocols},

author ={A.P. Marques Jr. and A.P. Ravn and J. Srba and S. Vighio},

journal ={International Journal on Software Tools for Technology Transfer (STTT)},

publisher ={Springer-Verlag},

year ={2013},

volume ={15},

number ={2},

pages ={125--147},

doi ={10.1007/s10009-012-0231-4},

issn ={1433-2779},

abstract ={Web Services Business Activity specification definestwo coordination protocols BAwCC (Business Agreement with Coordination Completion)and BAwPC (Business Agreement with Participant Completion)that ensure a consistent agreement on the outcome of long-running distributedapplications. In order to verify fundamental properties of the protocolswe provide formal analyses in the model checker UPPAAL.Our analyses are supported by a newly developed tool chain,where in the first step we translatetables with state-transition protocol descriptionsinto an intermediate XML format, and in the second step wetranslate this format into a network of communicating state machinesdirectly suitable for verification in UPPAAL.Our results show that the WS-BA protocols, as described in the standardspecification, violate correct operation by reaching invalid statesfor all underlying communication media except for a perfect FIFO.Hence we propose changes to the protocols and a furtherinvestigation of the modified protocols suggests that in case ofthe BAwCC protocol messages shouldbe received in the same order as they are sent to preserve correct behaviour,while BAwPC is now correct even for asynchronous,unordered, lossy and duplicating media.Another important property of communication protocolsis that all parties always reach, under certain fairness assumptions,their final states. Based on an automatic verification with differentcommunication models, we prove that our enhanced protocols satisfy thisproperty whereas the original protocols do not.All verification results presented in this article were performedin a fully automatic way using our new tool csv2uppaal.},

pdf ={http://www.cs.aau.dk/~srba/files/MRSV:sttt:2012.pdf},

ee ={http://dx.doi.org/10.1007/s10009-012-0231-4},

}

@article{BKLS:IC:12,

title ={EXPTIME-Completeness of Thorough Refinement on 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 ={Information and Computation},

publisher ={Elsevier},

year ={2012},

volume ={218},

pages ={54--68},

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 and deterministic.},

pdf ={http://www.cs.aau.dk/~srba/files/BKLS:IC:12.pdf},

ee ={http://dx.doi.org/10.1016/j.ic.2012.08.001},

}

@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 ={22},

number ={4},

pages ={581--617},

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.cs.aau.dk/~srba/files/BJLLS:MSCS:12.pdf},

ee ={http://dx.doi.org/10.1017/S0960129511000697},

}

@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.cs.aau.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.cs.aau.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.cs.aau.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.cs.aau.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.cs.aau.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.cs.aau.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.cs.aau.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.cs.aau.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.cs.aau.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.cs.aau.dk/~srba/files/S:TCS:01.pdf},

}

@techreport{BBLS:TechRep:15,

author ={N. Bene\v{s} and P. Bezdek and K.G. Larsen and J. Srba},

title ={Language Emptiness of Continuous-Time Parametric Timed Automata},

institution ={arXiv.org open access e-prints in Computer Science},

year ={2015},

number ={arXiv.org 1504.07838},

key ={arXiv.org 1504.07838},

pagecount ={19},

ee ={http://arxiv.org/abs/1504.07838},

abstract ={Parametric timed automata extend the standard timed automata withthe possibility to use parameters in the clock guards. In general, if theparameters are real-valued, the problem of language emptiness of such automatais undecidable even for various restricted subclasses. We thus focus on the casewhere parameters are assumed to be integer-valued, while the time still remainscontinuous. On the one hand, we show that the problem remains undecidable forparametric timed automata with three clocks and one parameter. On the other hand,for the case with arbitrary many clocks where only one of these clocks is comparedwith (an arbitrary number of) parameters, we show that the parametric languageemptiness is decidable. The undecidability result tightens the bounds of a previousresult which assumed six parameters, while the decidability result extends theexisting approaches that deal with discrete-time semantics only. To the best ofour knowledge, this is the first positive result in the case of continuous-timeand unbounded integer parameters, except for the rather simple case ofsingle-clock automata.},

}

@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.cs.aau.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.cs.aau.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.cs.aau.dk/~srba/files/Srba:master:98.pdf},

}

@proceedings{LS:nwpt:16,

author ={K.G. Larsen and J. Srba},

title ={Proceedings of the 28th Nordic Workshop on Programming Theory ({NWPT}'16)},

journal ={Aalborg University},

year ={2016},

ee ={http://nwpt2016.cs.aau.dk/nwpt2016-proceedings.pdf},

}

@proceedings{LPS:reachability:16,

author ={K.G. Larsen and I. Potapov and J. Srba},

title ={Proceedings of the 10th International Workshop on Reachability Problems ({RP}'16)},

journal ={LNCS},

volume ={9899},

year ={2016},

ee ={http://dx.doi.org/10.1007/978-3-319-45994-3},

}

@proceedings{BDJMS:cassting-syncop:16,

author ={T. Brihaye and B. Delahaye and L. Jezequel and N. Markey and J. Srba},

title ={Proceedings of Cassting Workshop on Games for the Synthesis of Complex Systems ({CASSTING}'16) and the 3rd International Workshop on Synthesis of Complex Parameters ({SynCoP}'16)},

journal ={EPTCS},

volume ={220},

year ={2016},

ee ={http://eptcs.web.cse.unsw.edu.au/content.cgi?CASSTINGSynCoP2016},

doi ={10.4204/EPTCS.220},

}

@proceedings{FJKSS:11:evaluation,

author ={H. Frahm and M. Jaeger and J. Kjeldskov and S. Saltenis and J. Srba},

title ={Research Evaluation 2006-2010, Computer Science},

journal ={Aalborg University},

year ={2011},

ee ={http://files.portal.aau.dk/filesharing/download?filename=person/carstennielsen/~/pub/ResearchEvaluation2006-2010.pdf},

isbn ={978-87-991383-1-9},

}

@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},

}