@inproceedings{MCC:24,
title ={Behind the Scene of the Model Checking Contest, Analysis of Results from 2018 to 2023},
author ={N. Amat and E. Amparore and B. Berthomieu and P. Bouvier and S. Zilio and F. Hulin-Hubard and P.G. Jensenand L. Jezequel and F. Kordon and S. Li and E. Paviot-Adet and L. Petrucci and J. Srba and Y. Thierry-Mieg and K. Wolf},
booktitle ={{TOOLympics} Challenge 2023},
year ={2024},
series ={LNCS},
volume ={14550},
publisher ={Springer},
pages ={52--89},
abstract ={This paper takes you behind the scenes of the Model Checking Contest (MCC), an annual competition focusing on the behavioral analysis of asynchronous systems using state-space exploration and model checking techniques.The MCC is part of a thriving group of scientific events dedicated to provide a fair evaluation of formal analysis tools, with the goal to push forward the state of the art and provide insights into the evolution of the involved technologies and approaches. We give details on the organization of the competition and on the ways we manage models and formulas. We also take a look at the evolution of the results over the 2018--2023 period, using the wide variety of data we collect each year, and report on the impact the MCC had on the competing tools.},
isbn ={978-3-031-67695-6},
pdf ={http://www.cs.aau.dk/~srba/files/MCC:24.pdf},
ee ={https://link.springer.com/chapter/10.1007/978-3-031-67695-6_3},
doi ={10.1007/978-3-031-67695-6_3},
}

@inproceedings{GLSS:DSN:2024,
author ={C. Gyorgyi and K.G. Larsen and S. Schmid and J. Srba},
title ={{SyRep}: Efficient Synthesis and Repair of Fast Re-Route Forwarding Tables for Resilient Networks},
booktitle ={Proceedings of the 54th Annual IEEE/IFIP International Conference on Dependable Systems and Networks ({DSN}'24)},
year ={2024},
publisher ={IEEE},
pages ={483--494},
abstract ={In modern communication networks with stringent dependability requirements, local fast re-routing (FRR) is essential for a quick response to link failures. Configuring FRR for multiple failures is, however, challenging since a router's forwarding table may take into account only the failed links directly incident to it. We propose SyRep, an efficient method to repair and synthesize resilient FRR forwarding tables. At the heart of SyRep lies a method which identifies and removes ill-defined routing entries and employs symbolic binary decision diagram (BDD) technology to automatically replace the removed entries with correct values. SyRep cannot only be used to efficiently repair existing forwarding tables, but also to synthesize new tables from scratch, using an efficient hybrid approach: by first using fast heuristics that provide close-to-resilient routing tables and then quickly repair the ill-defined entries. We present such a fast heuristic based on novel structural reduction rules and our empirical evaluation shows that SyRep is up to three orders of magnitude faster compared to the state-of-the-art.},
pdf ={http://www.cs.aau.dk/~srba/files/GLSS:DSN:24.pdf},
ee ={https://ieeexplore.ieee.org/document/10646937},
doi ={10.1109/DSN58291.2024.00053},
}

@inproceedings{INFOCOM:GLSS:24,
author ={C. Gyorgyi and K.G. Larsen and S. Schmid and J. Srba},
title ={{SyPer:} Synthesis of Perfectly Resilient Local Fast Re-Routing Rules for Highly Dependable Networks},
booktitle ={{IEEE} International Conference on Computer Communications ({INFOCOM}'24)},
pages ={2398--2407},
year ={2024},
publisher ={{IEEE}},
abstract ={Modern communication networks support local fast re-routing (FRR) to quickly react to link failures. However, configuring such FRR mechanisms is challenging as the ruleshave to be defined ahead of time, without knowledge of the failures, and can depend only on local decisions made by the nodes incident to a failed link. Designing failover protection against multiple link failures is particularly difficult. We presenta novel synthesis approach which addresses this challenge by generating FRR rules in an automated and provably correct manner. Our network model assumes that each node maintains a prioritised list of backup links (a.k.a. skipping forwarding)---an FRR method that allows for a memory-efficient deployment. We study the theoretical properties of the model and implement a synthesis method in our tool SyPer that aims to provide perfect resilience: if there are up to k link failures, we can always route traffic between any two nodes as long as they are still connected in the underlying physical network. To this end, SyPer focuses on the synthesis of efficient forwarding rules using the BDD (binary decision diagram) methodology and our empirical evaluation shows that SyPer is feasible, and can synthesize robust network configuration in realistic settings.},
pdf ={http://www.cs.aau.dk/~srba/files/INFOCOM:GLSS:24.pdf},
ee ={https://ieeexplore.ieee.org/document/10621323},
doi ={10.1109/INFOCOM52122.2024.10621323},
}

@inproceedings{SPS:PRDC:23,
author ={M.K. Schou and I. Poese and J. Srba},
title ={Discovery of Flow Splitting Ratios in ISP Networks with Measurement Noise},
booktitle ={Proceedings of the 28th IEEE Pacific Rim International Symposium on Dependable Computing ({PRDC}'23)},
year ={2023},
pages ={64--70},
publisher ={IEEE},
abstract ={Network telemetry and analytics is essential for providing highly dependable services in modern computer networks. In particular, network flow analytics for ISP networks allows operators to inspect and reason about traffic patterns in their networks in order to react to anomalies. High performance network analytics systems are designed with scalability in mind, and can consequently only observe partial information about the network traffic. Still, they need to provide a holistic view of the traffic, including the distribution of different traffic flows on each link. It is impractical to monitor such fine-grained telemetry, and in large, heterogeneous networks it is often too complex and error-prone, if not impossible, to access and maintain all technical specifications and router-specific configurations needed to determine e.g. the load balancing weights used when traffic is split onto multiple paths. The ratios by which flows are split on the possible paths must be derived indirectly from the measured flow demands and link utilizations. Motivated by a case study provided by a major European ISP, we suggest an efficient method to estimate the flow splitting ratios. Our approach, based on quadratic linear programming, is scalable and robust to the measurement noise found in a typical network analytics deployment. Finally, we implement an automated tool for estimating the flow splitting ratios and document its applicability on real data from the ISP.},
pdf ={http://www.cs.aau.dk/~srba/files/SPS:PRDC:23.pdf},
ee ={https://doi.ieeecomputersociety.org/10.1109/PRDC59308.2023.00017},
doi ={10.1109/PRDC59308.2023.00017},
}

@inproceedings{HJLS:FMICS:23,
author ={I.R. Hasrat and P.G. Jensen and K.G. Larsen and J. Srba},
title ={Modelling of Hot Water Buffer Tank and Mixing Loop for an Intelligent Heat Pump Control},
booktitle ={Proceedings of the 28th International Conference on Formal Methods for Industrial Critical Systems ({FMICS}'23)},
year ={2023},
series ={LNCS},
volume ={14290},
pages ={113--130},
publisher ={Springer-Verlag},
abstract ={The recent surge in electricity prices has increased the demand for cost-effective and sophisticated heat pump controllers. As domestic floor heating systems are becoming increasingly popular, there is an urgent need for more efficient control systems that include also heat buffer tanks to account for fluctuating energy prices. We propose a scalable thermal model of the hot water buffer tank together with a mixing loop and evaluate its operation and performance on an experimental Danish house from the OpSys project. We experimentally assess the buffer tank's quality by selecting the proper size and number of virtual layers using an industry-standard controller. Finally, we integrate the buffer tank and mixing loop into the heating system and create an intelligent Stratego controller to examine their performance. We analyze the tradeoff between cost and comfort for different buffer tank sizes to determine when a buffer tank or a mixing loop should be included in the system. By providing a detailed understanding of the buffer tank and mixing loop, our study enables the clients to make better decisions regarding the appropriate buffer tank size and when to install a mixing loop based on their specific heating needs.},
pdf ={http://www.cs.aau.dk/~srba/files/HJLS:FMICS:23.pdf},
ee ={https://link.springer.com/chapter/10.1007/978-3-031-43681-9_7},
doi ={10.1007/978-3-031-43681-9_7},
}

@inproceedings{JLSU:SPIN:23,
author ={P.G. Jensen and K.G. Larsen and J. Srba and N.J. Ulrik},
title ={Elimination of Detached Regions in Dependency Graph Verification},
booktitle ={Proceedings of the 29th International SPIN Symposium on Model Checking of Software ({SPIN}'23)},
year ={2023},
series ={LNCS},
volume ={13872},
pages ={163--179},
publisher ={Springer-Verlag},
abstract ={The formalism of dependency graphs by Liu and Smolka is a well-established method for on-the-fly computation of fixed points over Boolean domains with numerous applications in e.g. model checking, game synthesis, bisimulation checking and others. The original Liu and Smolka on-the-fly algorithm runs in linear time, and several extensions and improvements to this algorithm have recently been studied, including the notion of negation edges, certain-zero early termination as well as extensions towards abstract dependency graphs. We present a novel improvement for computing the least fixed-point assignment on dependency graphs, with the goal of avoiding the exploration of detached subgraphs that cannot contribute to the assignment value of the root node. We also experimentally evaluate different ways of resolving nondeterminism in the algorithm and execute experiments on CTL formulae from the annual Petri net model checking contest as well as on synthesis problems for Petri games. We find out that our algorithm significantly improves the state-of-the-art.},
pdf ={http://www.cs.aau.dk/~srba/files/JLSU:SPIN:23.pdf},
ee ={https://link.springer.com/chapter/10.1007/978-3-031-32157-3_9},
doi ={10.1007/978-3-031-32157-3_9},
}

@inproceedings{HKNRSSS:SPIN:23,
author ={E.G.Henriksen and A.M. Khorsid and E. Nielsen and Th. Risager and J. Srba and A.M. St\"{u}ck and S. S{\o}rensen},
title ={Potency-Based Heuristic Search with Randomness for Explicit Model Checking},
booktitle ={Proceedings of the 29th International SPIN Symposium on Model Checking of Software ({SPIN}'23)},
year ={2023},
series ={LNCS},
volume ={13872},
pages ={180--187},
publisher ={Springer-Verlag},
abstract ={Efficient state-space exploration has a significant impact on reachability analysis in explicit model checking and existing tools use several variants of search heuristics and random walks in order to overcome the state-space explosion problem. We contribute with a novel approach based on a random search strategy, where actions are assigned dynamically (on-the-fly) updated potencies, changing according to the variations of a heuristic distance to the goal configuration as encountered during the state-space search. We implement our general idea into a Petri net model checker TAPAAL and document its efficiency on a large benchmark of Petri net models from the annual Model Checking Contest. The experiments show that our heuristic search outperforms the standard search approaches in multiple metrics and that it constitutes a worthy addition to the portfolio of classical search strategies.},
pdf ={http://www.cs.aau.dk/~srba/files/HKNRSSS:SPIN:23.pdf},
ee ={https://link.springer.com/chapter/10.1007/978-3-031-32157-3_10},
doi ={10.1007/978-3-031-32157-3_10},
}

@inproceedings{SSSV:CONEXT:22,
author ={S. Schmid and M.K. Schou and J. Srba and J. Vanerio},
title ={{R-MPLS}: Recursive Protection for Highly Dependable {MPLS} Networks},
booktitle ={Proceedings of the 18th International Conference on Emerging Networking EXperiments and Technologies ({CoNEXT'22})},
year ={2022},
pages ={276--292},
publisher ={ACM},
abstract ={Most modern communication networks feature fast rerouting mechanisms in the data plane. However, design and configuration of such mechanisms even under multiple failures is known to be difficult. In order to increase the resilience of the widely deployed MPLS networks, we propose R-MPLS, an alternative link protection mechanism for MPLS networks that uses recursive protection and can route around multiple simultaneously failed links. Our new R-MPLS approach comes with strong theoretical underpinnings, is implementable in a fully distributed way and executable on existing MPLS hardware, and formally guarantees that no forwarding loops are introduced. We implement our R-MPLS protection in an automated tool which overcomes the complexity of configuring such resilient network data planes, and report on the benefits of recursive protection in realistic network topologies. We find that R-MPLS significantly increases network robustness against multiple failures, with only moderate increase in the number of forwarding rules and communication overhead (both comparable to industry- standards like RSVP-TE FRR).},
pdf ={http://www.cs.aau.dk/~srba/files/SSSV:CONEXT:22.pdf},
ee ={https://dl.acm.org/doi/10.1145/3555050.3569140},
doi ={10.1145/3555050.3569140},
}

@inproceedings{VSSS:GI:22,
author ={J. Vanerio and S. Schmid and M.K. Schou and J. Srba},
title ={MPLS-Kit: An MPLS Data Plane Toolkit},
booktitle ={IEEE Global Internet (GI) Symposium 2022},
year ={2022},
pages ={49--54},
publisher ={IEEE},
abstract ={Networking research often requires a means to quickly generate different realistic networks for evaluatingthe practical relevance. This is especially the case for emerging fields related to the automated verification ofnetwork configurations (what-if analysis) or to AI-driven network operations (self-driving networks).Unfortunately, the data of real world network deployments are often scarce. In particular, while the topologies ofmany real communication networks have been made available online, this data typically does not include the routers'forwarding tables, e.g., by Internet Service Providers (ISPs). This introduces a dilemma, as generating arbitraryforwarding rules for these topologies may not adequately mimic network behavior. We present MPLS-Kit, a tool for theautomated generation of realistic MPLS data planes. In particular, the tool supports an efficient generation of MPLS dataplanes following widely-deployed industry-standard control protocols on top of arbitrary network topologies.Notably, MPLS-Kit supports the instantiation of MPLS Fast Reroute and VPN services. It further supports packet-levelsimulations providing a rich set of statistics about the simulated data plane which can be used for numerous applications,like congestion, latency, and resilience analysis. The generated data planes can be further exported in standard exchangeformats and analyzed by formal verification tools.},
pdf ={http://www.cs.aau.dk/~srba/files/VSSS:GI:2022.pdf},
ee ={https://ieeexplore.ieee.org/document/9978791/},
doi ={10.1109/CloudNet55617.2022.9978791},
}

@inproceedings{JKMNSST:GI:22,
author ={N.S. Johansen and L.B. Kaer and A.L. Madsen and K.O. Nielsen and S. Schmid and J. Srba and R.G. Tollund},
title ={FBR: Dynamic Memory-Aware Fast Rerouting},
booktitle ={IEEE Global Internet (GI) Symposium 2022},
year ={2022},
pages ={55--60},
publisher ={IEEE},
abstract ={Modern internet communication networks, such as MPLS networks, provide fast rerouting mechanisms in the data plane in order to quickly react to link failures and hence become more dependable. However, fast rerouting requires additional memory for the conditional failover rules---a scarce and expensive resource. We initiate the study of memory-aware fast rerouting mechanisms and present Forward-Backward Routing (FBR), a dynamic rerouting approach with a provably high resilience to multiple link failures, which accounts for memory constraints on the routers. FBR relies on backtracking search along the routing paths via packet header modifications, and in our experimential evaluation on a wide range of ISP topologies, it outperforms state-of-the-art solutions while using less memory.},
pdf ={http://www.cs.aau.dk/~srba/files/JKMNSST:GI:2022.pdf},
ee ={https://ieeexplore.ieee.org/document/9978819},
doi ={10.1109/CloudNet55617.2022.9978819},
}

@inproceedings{LSS:Henzinger60:22,
author ={K.G. Larsen and Ch. Schilling and J. Srba},
title ={Simulation Relations and Applications in Formal Methods},
booktitle ={Principles of Systems Design: Essays Dedicated to Thomas A. Henzinger on the Occasion of His 60th Birthday},
year ={2022},
pages ={272--291},
series ={LNCS},
volume ={13660},
publisher ={Springer},
abstract ={We survey the research on application of equivalence checking to formal methods, with a particular focus on the notion of simulation and bisimulation as well as of modal refinement on modal transition systems. We discuss the algorithmic aspects of efficiently computing (bi)simulation relations, the extension to infinite state systems, and existing tool support. We then present results related to simulation and bisimulation checking on timed and hybrid systems and highlight the connections to automata theory.},
pdf ={http://www.cs.aau.dk/~srba/files/LSS:Henzinger60:22.pdf},
ee ={https://link.springer.com/chapter/10.1007/978-3-031-22337-2_13},
doi ={10.1007/978-3-031-22337-2_13},
}

@inproceedings{SSST:FMCAD:22,
author ={A. Schlichtkrull and M.K. Schou and J. Srba and D. Traytel},
title ={Differential Testing of Pushdown Reachability with a Formally Verified Oracle},
booktitle ={Proceedings of the 22nd Conference on Formal Methods in Computer-Aided Design ({FMCAD}'22)},
year ={2022},
pages ={369--379},
publisher ={TU Wien Academic Press},
abstract ={Pushdown automata are an essential model of recursive computation. In model checking and static analysis, numerous problems can be reduced to reachability questions about pushdown automata and several efficient libraries implement automata-theoretic algorithms for answering these questions. These libraries are often used as core components in other tools, and therefore it is instrumental that the used algorithms and their implementations are correct. We present a method that significantly increases the trust in the answers provided by the libraries for pushdown reachability by (i) formally verifying the correctness of the used algorithms using the Isabelle/HOL proof assistant, (ii) extracting executable programs from the formalization, (iii) implementing a framework for the differential testing of library implementations with the verified extracted algorithms as oracles, and (iv) automatically minimizing counter-examples from the differential testing based on the delta-debugging methodology. We instantiate our method to the concrete case of PDAAAL, a state-of-the-art library for pushdown reachability. Thereby, we discover and resolve several nontrivial errors in PDAAAL.},
pdf ={http://www.cs.aau.dk/~srba/files/SSST:FMCAD:22.pdf},
ee ={https://repositum.tuwien.at/handle/20.500.12708/81373},
doi ={10.34727/2022/isbn.978-3-85448-053-2_44},
}

@inproceedings{GJLSZ:ATVA:22,
author ={M.A. Goorden and P.G. Jensen and K.G. Larsen and M. Samusev and J. Srba and G. Zhao},
title ={{STOMPC}: Stochastic Model-Predictive Control with Uppaal Stratego},
booktitle ={Proceedings of the 20th International Symposium on Automated Technology for Verification and Analysis ({ATVA}'22)},
year ={2022},
series ={LNCS},
volume ={13505},
publisher ={Springer-Verlag},
pages ={327--333},
abstract ={We present the new co-simulation and synthesis integrated-framework STOMPC for stochastic model-predictive control (MPC) with Uppaal Stratego. The framework allows users to easily set up MPC designs, a widely accepted method for designing software controllers in industry, with Uppaal Stratego as the controller synthesis engine, which provides a powerful tool to synthesize safe and optimal strategies for hybrid stochastic systems. STOMPC provides the user freedom to connect it to external simulators, making the framework applicable across multiple domains.},
pdf ={http://www.cs.aau.dk/~srba/files/GJLSZ:ATVA:22.pdf},
ee ={https://link.springer.com/chapter/10.1007/978-3-031-19992-9_21},
doi ={10.1007/978-3-031-19992-9_21},
}

@inproceedings{JSSS:ATVA:22,
author ={P.G. Jensen and S. Schmid and M.K. Schou and J. Srba},
title ={{PDAAAL}: A Library for Reachability Analysis of Weighted Pushdown Systems},
booktitle ={Proceedings of the 20th International Symposium on Automated Technology for Verification and Analysis ({ATVA}'22)},
year ={2022},
series ={LNCS},
volume ={13505},
publisher ={Springer-Verlag},
pages ={225--230},
abstract ={We present PDAAAL, an open source C++ library and tool for weighted reachability analysis of pushdown systems, including generation of both shortest and longest witness traces. We consider totally ordered weight domains which have important applications, e.g. in network verification, and achieve a speedup of two orders of magnitude compared to the state-of-the-art tool WALi. Our tool further extends the state of the art by supporting the generation of the longest trace in case it exists, or reporting that no finite longest trace can be generated. PDAAAL is provided both as a stand-alone tool accepting JSON files and as a C++ library. This allows for integration in software pipelines as well as in verification tools like AalWiNes.},
pdf ={http://www.cs.aau.dk/~srba/files/JSSS:ATVA:22.pdf},
ee ={https://link.springer.com/chapter/10.1007/978-3-031-19992-9_14},
doi ={10.1007/978-3-031-19992-9_14},
}

@inproceedings{HJLS:TASE:22,
author ={I.R. Hasrat and P.G. Jensen and K.G. Larsen and J. Srba},
title ={End-to-End Heat-Pump Control Using Continuous Time Stochastic Modelling and Uppaal Stratego},
booktitle ={Proceedings of the 16th International Symposium on Theoretical Aspects of Software Engineering ({TASE}'22)},
year ={2022},
series ={LNCS},
volume ={13299},
pages ={363--380},
publisher ={Springer},
abstract ={Heatpump-based floor-heating systems for domestic heating offer flexibility in energy-consumption patterns, which can be utilized for reducing heating costs---in particular when considering hour-based electricity prices. Such flexibility is hard to exploit via classical Model Predictive Control (MPC), and in addition, MPC requires a priori calibration (i.e. model identification) which is often costly and becomes outdated as the dynamics and use of a building change. We solve these shortcomings by combining recent advancements in stochastic model identification and automatic (near-)optimal controller synthesis. Our method suggests an adaptive model-identification using the tool CTSM-R, and an efficient control synthesis based on Q-learning for Euclidean Markov Decision Processes via Uppaal Stratego. On a virtual Danish family-house from the OpSys project, we demonstrate up to 33 percent reduction in heating cost while retaining comparable comfort to a standard bang-bang controller. Furthermore, we show the flexibility of our method by computing the Pareto-frontier that visualizes the cost/comfort tradeoff.},
pdf ={http://www.cs.aau.dk/~srba/files/HJLS:TASE:22.pdf},
ee ={https://link.springer.com/chapter/10.1007/978-3-031-10363-6_24},
doi ={10.1007/978-3-031-10363-6_24},
}

@inproceedings{LMSS:TASE:22,
author ={K.G. Larsen and A. Mariegaard and S. Schmid and J. Srba},
title ={AllSynth: Transiently Correct Network Update Synthesis Accounting for Operator Preferences},
booktitle ={Proceedings of the 16th International Symposium on Theoretical Aspects of Software Engineering ({TASE}'22)},
year ={2022},
pages ={344--362},
series ={LNCS},
volume ={13299},
publisher ={Springer},
abstract ={The increasingly stringent dependability requirements on communication networks as well as the need to render these networks more adaptive to improve performance, demand for more automated approaches to operate networks. We present AllSynth, a symbolic synthesis tool for updating communication networks in a provably correct and efficient manner. AllSynth automatically synthesizes network update schedules which transiently ensure a wide range of policy properties (expressed in the LTL logic), also during the reconfiguration process. In particular, in contrast to existing approaches, AllSynth symbolically computes and compactly represents all feasible solutions. At its heart, AllSynth relies on a novel, two-level and parameterized use of BDDs which greatly improves performance. Indeed, AllSynth not only provides formal correctness guarantees and outperforms existing state-of-the-art tools in terms of generality, but often also in terms of runtime as documented by experiments on a benchmark of real-world network topologies.},
pdf ={http://www.cs.aau.dk/~srba/files/LMSS:TASE:22.pdf},
ee ={https://link.springer.com/chapter/10.1007/978-3-031-10363-6_23},
doi ={10.1007/978-3-031-10363-6_23},
}

@inproceedings{CSSS:DSN:2022,
author ={P. Cuijpers and S. Schmid and N. Schnepf and J. Srba},
title ={The Hazard Value: A Quantitative Network Connectivity Measure Accounting for Failures},
booktitle ={Proceedings of the 52nd Annual IEEE/IFIP International Conference on Dependable Systems and Networks ({DSN}'22)},
year ={2022},
publisher ={IEEE},
pages ={239--250},
abstract ={To meet their stringent requirements in terms of performance and dependability, communication networks should be "well connected". While classic connectivity measures typically revolve around topological properties, e.g., related to cuts, these measures may not reflect well the degree to which a network is actually dependable. We introduce a more refined measure for network connectivity, the hazard value, which is developed to meet the needs of a real network operator. It accounts for crucial aspects affecting the dependability experienced in practice, including actual traffic patterns, distribution of failure probabilities, routing constraints, and alternatives for services with preferences therein. We analytically show that the hazard value fulfills several fundamental desirable properties that make it suitable for comparing different network topologies with one another, and for reasoning about how to efficiently enhance the robustness of a given network. We also present an optimised algorithm to compute the hazard value and an experimental evaluation against networks from the Internet Topology Zoo and classical datacenter topologies, such as fat trees and BCubes. This evaluation shows that the algorithm computes the hazard value within minutes for realistic networks, making it practically usable for network designers.},
pdf ={http://www.cs.aau.dk/~srba/files/CSSS:DSN:22.pdf},
ee ={https://ieeexplore.ieee.org/document/9833715},
doi ={10.1109/DSN53405.2022.00034},
}

@inproceedings{JKMNST:iFM:2022,
author ={N.S. Johansen and L.B. Kaer and A.L. Madsen and K.O. Nielsen and J. Srba and R.G. Tollund},
title ={Kaki: Concurrent Update Synthesis for Regular Policies via Petri Games},
booktitle ={Proceedings of the 17th International Conference on Integrated Formal Methods ({iFM'22})},
year ={2022},
series ={LNCS},
volume ={13274},
publisher ={Springer-Verlag},
pages ={249--267},
abstract ={Modern computer networks are becoming increasingly complex and for dependability reasons require frequent configuration changes. It is essential that forwarding policies are preserved not only before and after the configuration update but also at any moment during the inherently distributed execution of the update. We present Kaki, a Petri game based approach for automatic synthesis of switch batches that can be updated in parallel without violating a given (regular) forwarding policy like waypointing and service chaining. Kaki guarantees to find the minimum number of concurrent batches and it supports both splittable and nonsplittable flow forwarding. In order to achieve an optimal performance, we introduce two novel optimization techniques based on static analysis: decomposition into independent subproblems and identification of switches that can be collectively updated in the same batch. These techniques considerably improve the performance of our tool, relying on TAPAAL's verification engine for Petri games as its backend. Experiments on a large benchmark of real networks from the topology Zoo database demonstrate that Kaki outperforms the state-of-the-art tool FLIP as it provides shorter (and provably optimal) concurrent update sequences at similar runtime.},
pdf ={http://www.cs.aau.dk/~srba/files/JKMNST:iFM:22.pdf},
ee ={https://link.springer.com/chapter/10.1007/978-3-031-07727-2_14},
doi ={10.1007/978-3-031-07727-2_14},
}

@inproceedings{JSUV:VMCAI:2022,
author ={P.G. Jensen and J. Srba and N.J. Ulrik and S.M. Virenfeldt},
title ={Automata-Driven Partial Order Reduction and Guided Search for LTL Model Checking},
booktitle ={Proceedings of the 23rd International Conference on Verification, Model Checking, and Abstract Interpretation ({VMCAI}'22)},
year ={2022},
series ={LNCS},
volume ={13182},
publisher ={Springer-Verlag},
pages ={151--173},
abstract ={In LTL model checking, a system model is synchronized using the product construction with Buchi automaton representing all runs that invalidate a given LTL formula. An existence of a run with infinitely many occurrences of an accepting state in the product automaton then provides a counter-example to the validity of the LTL formula. Classical partial order reduction methods for LTL model checking allow to considerably prune the searchable state space, however, the majority of published approaches do not use the information about the current Buchi state in the product automaton. We demonstrate that this additional information can be used to significantly improve the performance of existing techniques. In particular, we present a novel partial order method based on stubborn sets and a heuristically guided search, both driven by the information of the current state in the Buchi automaton. We implement these techniques in the model checker TAPAAL and an extensive benchmarking on the dataset of Petri net models and LTL formulae from the 2021 Model Checking Contest documents that the combination of the automata-driven stubborn set reduction and heuristic search improves the state-of-the-art techniques by a significant margin.},
pdf ={http://www.cs.aau.dk/~srba/files/JSUV:VMCAI:22.pdf},
ee ={https://link.springer.com/chapter/10.1007/978-3-030-94583-1_8},
doi ={10.1007/978-3-030-94583-1_8},
}

@inproceedings{BJPST:RP:2021,
author ={A. Bilgram and P.G. Jensen and T. Pedersen and J. Srba and P.H. Taankvist},
title ={Improvements in Unfolding of Colored Petri Nets},
booktitle ={Proceedings of the 15th International Conference on Reachability Problems ({RP}'21)},
year ={2021},
series ={LNCS},
volume ={13035},
publisher ={Springer-Verlag},
pages ={69--84},
abstract ={Colored Petri nets offer a compact and user friendly representation of the traditional P/T nets and colored nets with finite color ranges can be unfolded into the underlying P/T nets, however, at the expense of an exponential explosion in size. We present two novel techniques based on static analyses in order to reduce the size of unfolded colored nets. The first method identifies colors that behave equivalently and groups them into equivalence classes, potentially reducing the number of used colors. The second method overapproximates the sets of colors that can appear in places and excludes colors that can never be present in a given place. Both methods are complementary and the combined approach allows us to significantly reduce the size of multiple colored Petri nets from the Model Checking Contest benchmark. We compare the performance of our unfolder with state-of-the-art techniques implemented in the tools MCC, Spike and ITS-Tools, and while our approach remains competitive w.r.t. unfolding time, it outperforms the existing approaches both in the size of unfolded nets as well as in the number of answered model checking queries from the 2020 Model Checking Contest.},
pdf ={http://www.cs.aau.dk/~srba/files/BJPST:RP:2021.pdf},
ee ={https://link.springer.com/chapter/10.1007/978-3-030-89716-1_5},
doi ={10.1007/978-3-030-89716-1_5},
}

@inproceedings{JSSSVD:ATVA:21,
author ={P.G. Jensen and S. Schmid and M.K. Schou and J. Srba and J. Vanerio and I. van Duijn},
title ={Faster Pushdown Reachability Analysis with Applications in Network Verification},
booktitle ={Proceedings of the 19th International Symposium on Automated Technology for Verification and Analysis ({ATVA}'21)},
year ={2021},
series ={LNCS},
volume ={12971},
publisher ={Springer-Verlag},
pages ={170--186},
abstract ={Reachability analysis of pushdown systems is a fundamental problem in model checking that comes with a wide range of applications. We study performance improvements of pushdown reachability analysis and as a case study, we consider the verification of the policy-compliance of MPLS (Multiprotocol Label Switching) networks, an application domain that has recently received much attention. Our main contribution are three techniques that allow us to speed up the state-of-the-art pushdown reachability tools by an order of magnitude. These techniques include the combination of classic pre* and post* saturation algorithms into a dual-search algorithm, an on-the-fly technique for detecting the possibility of early termination, as well as a counter-example guided abstraction refinement technique that improves the performance in particular for the negative instances where the early termination technique is not applicable. As a second contribution, we describe an improved translation of MPLS networks to pushdown systems and demonstrate on an extensive set of benchmarks of real internet wide-area networks the efficiency of our approach.},
pdf ={http://www.cs.aau.dk/~srba/files/JSSSVD:ATVA:21.pdf},
ee ={https://link.springer.com/chapter/10.1007/978-3-030-88885-5_12},
doi ={10.1007/978-3-030-88885-5_12},
}

@inproceedings{MJLMS:FORMATS:21,
author ={F.M. Boenneland and P.G. Jensen and K.G. Larsen and M. Muniz and J. Srba},
title ={Stubborn Set Reduction for Timed Reachability and Safety Games},
booktitle ={Proceedings of the 19th International Conference on Formal Modelling and Analysis of Timed Systems (FORMATS'21)},
year ={2021},
series ={LNCS},
volume ={12860},
pages ={32--49},
publisher ={Springer-Verlag},
abstract ={Timed games are an essential formalism for modeling time-sensitive reactive systems that must respond to uncontrollable events triggered by the (hostile) environment. However, the control synthesis problem for these systems is often resource-demanding due to the state space explosion problem. To counter this problem, we present an extension of partial order reduction, based on stubborn sets, into timed games. We introduce the theoretical foundations on the general formalism of timed game labeled transition systems and then instantiate it to the model of timed-arc Petri net games. We provide an efficient implementation of our method as part of the model checker TAPAAL and discuss an experimental evaluation on several case studies that show increasing (sometimes even exponential) savings in time and memory as the case studies scale to larger instances. To the best of our knowledge, this is the first application of partial order reductions to a game formalism that includes time.},
pdf ={http://www.cs.aau.dk/~srba/files/BJLMS:FORMATS:21.pdf},
ee ={https://link.springer.com/chapter/10.1007%2F978-3-030-85037-1_3},
doi ={10.1007/978-3-030-85037-1_3},
}

@inproceedings{GLNNRS:ADHS:21,
author ={M.A. Goorden and K.G. Larsen and J.E. Nielsen and T.D. Nielsen and M.R. Rasmussen and J. Srba},
title ={Learning Safe and Optimal Control Strategies for Storm Water Detention Ponds},
booktitle ={Proceedings of the 7th IFAC Conference on Analysis and Design of Hybrid Systems ({ADHS}'21)},
year ={2021},
series ={IFAC-PapersOnLine},
volume ={54},
number ={5},
pages ={13--18},
publisher ={Elsevier},
abstract ={Storm water detention ponds are used to manage the discharge of rainfall runoff from urban areas to nearby streams. Their purpose is to reduce the hydraulic impact and sediment loads of the receiving waters. Detention ponds are currently designed based on static controls: the output flow of a pond is capped at a fixed value. This is not optimal with respect to the current infrastructure capacity and for some detention ponds it might even violate current regulations set by the European Water Framework Directive. We apply formal methods to synthesize (i.e., derive automatically) a safe and optimal active controller. We model the storm water detention pond, including the urban catchment area and the rain forecasts, as a hybrid Markov decision process. Subsequently, we use the tool Uppaal Stratego to synthesize a control strategy minimizing the cost related to pollution (optimality) while guaranteeing no emergency overflow of the detention pond (safety). Simulation results for an existing pond show that Uppaal Stratego can learn optimal strategies that prevent emergency overflows, where the current static control is not always able to prevent it. At the same time, our approach can improve sedimentation during low rain periods.},
pdf ={http://www.cs.aau.dk/~srba/files/GLNNRS:ADHS:21.pdf},
ee ={https://www.sciencedirect.com/science/article/pii/S2405896321012428?via%3Dihub},
doi ={10.1016/j.ifacol.2021.08.467},
}

@inproceedings{DJJKLLSS:PetriNets:21,
author ={M. Didriksen and P.G. Jensen and J.F. J{\o}nler and A.-I. Katona and S.D.L. Lama and F.B. Lottrup and S. Shajarat and J. Srba},
title ={Automatic Synthesis of Transiently Correct Network Updates via {Petri} Games},
booktitle ={Proceedings of the 42nd International Conference on Application and Theory of {P}etri Nets and Concurrency ({Petri Nets}'21)},
year ={2021},
series ={LNCS},
volume ={12734},
pages ={118--137},
publisher ={Springer-Verlag},
abstract ={As software-defined networking (SDN) is growing increasingly common within the networking industry, the lack of accessible and reliable automated methods for updating network configurations becomes more apparent. Any computer network is a complex distributed system and changes to its configuration may result in policy violations during the transient phase when the individual routers update their forwarding tables. We present an approach for automatic synthesis of update sequences that ensures correct network functionality throughout the entire update phase. Our approach is based on a novel translation of the update synthesis problem into a Petri game and it is implemented on top of the open-source model checker TAPAAL. On a large benchmark of synthetic and real-world network topologies, we document the efficiency of our approach and compare its performance with state-of-the-art tool NetSynth. Our experiments show that for several networks with up to thousands of nodes, we are able to outperform NetSynth's update schedule generation.},
pdf ={http://www.cs.aau.dk/~srba/files/DJJKLLSS:PetriNets:21.pdf},
ee ={https://link.springer.com/chapter/10.1007%2F978-3-030-76983-3_7},
doi ={10.1007/978-3-030-76983-3_7},
}

@inproceedings{SSS:TACAS:21,
author ={S. Schmid and N. Schnepf and J. Srba},
title ={Resilient Capacity-Aware Routing},
booktitle ={Proceedings of the 25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems ({TACAS}'21)},
year ={2021},
series ={LNCS},
volume ={12651},
publisher ={Springer-Verlag},
pages ={411--429},
abstract ={To ensure a high availability, communication networks provide resilient routing mechanisms that quickly change routes upon failures. However, a fundamental algorithmic question underlying such mechanisms is hardly understood: how to verify whether a given network reroutes flows along feasible paths, without violating capacity constraints, for up to k link failures? We chart the algorithmic complexity landscape of resilient routing under link failures, considering shortest path routing based on link weights as e.g. deployed in the ECMP protocol. We study two models: a pessimistic model where flows interfere in a worst-case manner along equal-cost shortest paths, and an optimistic model where flows are routed in a best-case manner, and we present a complete picture of the algorithmic complexities.We further propose a strategic search algorithm that checks only the critical failure scenarios while still providing correctness guarantees. Our experimental evaluation on a benchmark of Internet and datacenter topologies confirms an improved performance of our strategic search by several orders of magnitude.},
pdf ={http://www.cs.aau.dk/~srba/files/SSS:TACAS:21.pdf},
ee ={https://link.springer.com/chapter/10.1007%2F978-3-030-72016-2_22},
doi ={10.1007/978-3-030-72016-2_22},
}

@inproceedings{CGSS:PERFORMANCE:20,
author ={N. Christesen and M. Glavind and S. Schmid and J. Srba},
title ={Latte: Improving the Latency of Transiently Consistent Network Update Schedules},
booktitle ={Proceedings of 38th International Symposium on Computer Performance, Modeling, Measurements and Evaluation ({PERFORMANCE}'20)},
year ={2020},
series ={ACM SIGMETRICS Performance Evaluation Review},
volume ={48, no. 3},
publisher ={ACM},
pages ={14--26},
abstract ={Emerging software-defined and programmable networking technologies enable more adaptive communication infrastructures. However, leveraging these flexibilities and operating networks more adaptively is challenging, as the underlying infrastructure remains a complex distributed system that is a subject to delays, and as consistency properties need to be preserved transiently, even during network reconfiguration. Motivated by these challenges, we propose Latte, an automated approach to minimize the latency of network update schedules by avoiding unnecessary waiting times and exploiting concurrency, while at the same time provably ensuring a wide range of fundamental consistency properties like waypoint enforcement. To enable automated reasoning about the performance and consistency of software-defined networks during an update, we introduce the model of timed-arc colored Petri nets: an extension of Petri nets which allows us to account for time aspects in asynchronous networks, including characteristic timing behaviors, modeled as timed and colored tokens. This novel formalism may be of independent interest. Latte relies on an efficient translation of specific network update problems into timed-arc colored Petri nets. We show that the constructed nets can be analyzed efficiently via their unfolding into existing timed-arc Petri nets. We integrate Latte into the state-of-the-art model checking tool TAPAAL, and find that in many cases, we are able to reduce the latency of network updates by 90% or more.},
pdf ={http://www.cs.aau.dk/~srba/files/CGSS:PERFORMANCE:20.pdf},
ee ={https://dl.acm.org/doi/10.1145/3453953.3453957},
doi ={10.1145/3453953.3453957},
}

@inproceedings{EJLMS:LOPSTR:20,
author ={S. Enevoldsen and M.C. Jensen and K.G. Larsen and A. Mariegaard and J. Srba},
title ={Verification of Multiplayer Stochastic Games via Abstract Dependency Graphs},
booktitle ={Proceedings of the 30th International Symposium on Logic-Based Program Synthesis and Transformation ({LOPSTR}'20)},
year ={2020},
pages ={249--268},
series ={LNCS},
volume ={12561},
publisher ={Springer},
abstract ={We design and implement an efficient model checking algorithm for alternating-time temporal logic (ATL) on turn-based multiplayer stochastic games with weighted transitions. This logic allows us to query about the existence of multiplayer strategies that aim to maximize the probability of game runs satisfying resource-bounded next and until logical operators, while requiring that the accumulated weight along the successful runs does not exceed a given upper bound. Our method relies on a recently introduced formalism of abstract dependency graphs (ADG) and we provide an efficient reduction of our model checking problem to finding the minimum fixed-point assignment on an ADG over the domain of unit intervals extended with certain-zero optimization. As the fixed-point computation on ADGs is performed in an on-the-fly manner without the need of a priori generating the whole graph, we achieve a performance that is comparable with state-of-the-art model checker PRISM-games for finding the exact solutions and sometimes an order of magnitude faster for queries that ask about approximate probability bounds. We document this on a series of scalable experiments from the PRISM-games benchmark that we annotate with weight information.},
pdf ={http://www.cs.aau.dk/~srba/files/EJLMS:LOPSTR:20.pdf},
ee ={https://link.springer.com/chapter/10.1007%2F978-3-030-68446-4_13},
doi ={10.1007/978-3-030-68446-4_13},
}

@inproceedings{JKSSSS:CONEXT:20,
author ={P.G. Jensen and D. Kristiansen and S. Schmid and M.K. Schou and B.C. Schrenk and J. Srba},
title ={AalWiNes: A Fast and Quantitative What-If Analysis Tool for MPLS Networks},
booktitle ={Proceedings of the 16th International Conference on Emerging Networking EXperiments and Technologies ({CoNEXT'20})},
year ={2020},
pages ={474--481},
publisher ={ACM},
abstract ={We present an automated what-if analysis tool AalWiNes for MPLS networks which allows us to verify both logical properties (e.g., related to the policy compliance) as well as quantitative properties (e.g., concerning the latency) under multiple link failures. Our tool relies on weighted pushdown automata, a quantitative extension of classic automata theory, and takes into account the actual dataplane configuration, rendering it especially useful for debugging. In particular, our tool collects the different router forwarding tables and then builds a pushdown system, on which quantitative reachability is performed based on an expressive query language. Our experiments show that our tool outperforms state-of-the-art approaches (which until now have been restricted to logical properties) by several orders of magnitude; furthermore, our quantitative extension only entails a moderate overhead in terms of runtime. The tool comes with a platform-independent user interface and is publicly available as open-source, together with all other experimental artefacts.},
pdf ={http://www.cs.aau.dk/~srba/files/JKSSSS:CONEXT:20.pdf},
ee ={https://dl.acm.org/doi/10.1145/3386367.3431308},
doi ={10.1145/3386367.3431308},
}

@inproceedings{BKLMS:ATVA:11,
author ={K.G. Larsen and M. Mikucionis and M. Muniz and J. Srba},
title ={Urgent Partial Order Reduction for Extended Timed Automata},
booktitle ={Proceedings of the 18th International Symposium on Automated Technology for Verification and Analysis ({ATVA}'20)},
year ={2020},
series ={LNCS},
volume ={12302},
publisher ={Springer-Verlag},
pages ={179--195},
abstract ={We propose a partial order reduction method for reachability analysis of networks of timed automata interacting via synchronous channel communication and via shared variables. Our method is based on (classical) symbolic delay transition systems and exploits the urgent behavior of a system, where time does not introduce dependencies among actions. In the presence of urgent behavior in the network, we apply partial order reduction techniques for discrete systems based on stubborn sets. We first describe the framework in the general setting of symbolic delay time transition systems and then instantiate it to the case of timed automata. We implement our approach in the model checker Uppaal and observe a substantial reduction in the reachable state space for case studies that exhibit frequent urgent behaviour and only a moderate slowdown on models with limited occurence of urgency.},
pdf ={http://www.cs.aau.dk/~srba/files/LMMS:ATVA:20.pdf},
ee ={https://link.springer.com/chapter/10.1007/978-3-030-59152-6_10},
doi ={10.1007/978-3-030-59152-6_10},
}

@inproceedings{KLS:PN:20,
author ={I. Kaufmann and K.G. Larsen and J. Srba},
title ={Synthesis for Multi-Weighted Games with Branching-Time Winning Conditions},
booktitle ={Proceedings of the 41st International Conference on Application and Theory of {P}etri Nets and Concurrency ({Petri Nets}'20)},
year ={2020},
series ={LNCS},
volume ={12152},
pages ={46--66},
publisher ={Springer-Verlag},
abstract ={We investigate the synthesis problem in a quantitative game-theoretic setting with branching-time objectives. The objectives are given in a recursive modal logic with semantics defined over a multi-weighted extension of a Kripke structure where each transition is annotated with multiple nonnegative weights representing quantitative resources such as discrete time, energy and cost. The objectives may express bounds on the accumulation of each resource both in a global scope and in a local scope (on subformulae) utilizing a reset operator. We show that both the model checking problem as well as the synthesis problem are decidable and that the model checking problem is EXPTIME-complete, while the synthesis problem is in 2-EXPTIME and is NEXPTIME-hard. Furthermore, we encode both problems to the calculation of maximal fixed points on dependency graphs, thus achieving on-the-fly algorithms with the possibility of early termination.},
pdf ={http://www.cs.aau.dk/~srba/files/KLS:PN:20.pdf},
ee ={https://link.springer.com/chapter/10.1007/978-3-030-51831-8_3},
doi ={10.1007/978-3-030-51831-8_3},
}

@inproceedings{KLMS:PN:20,
author ={S.L. Karra and K.G. Larsen and M. Muniz and J. Srba},
title ={On-the-Fly Synthesis for Strictly Alternating Games},
booktitle ={Proceedings of the 41st International Conference on Application and Theory of {P}etri Nets and Concurrency ({Petri Nets}'20)},
year ={2020},
series ={LNCS},
volume ={12152},
pages ={109--128},
publisher ={Springer-Verlag},
abstract ={We study two-player zero-sum infinite reachability games with strictly alternating moves of the players allowing us to model a race between the two opponents. We develop an algorithm for deciding the winner of the game and suggest a notion of alternating simulation in order to speed up the computation of the winning strategy. The theory is applied to Petri net games, where the strictly alternating games are in general undecidable. We consider soft bounds on Petri net places in order to achieve decidability and implement the algorithms in our prototype tool. Finally, we compare the performance of our approach with an algorithm proposed in the seminal work by Liu and Smolka for calculating the minimum fixed points on dependency graphs. The results show that using alternating simulation almost always improves the performance in time and space and with exponential gain in some examples. Moreover, we show that there are Petri net games where our algorithm with alternating simulation terminates, whereas the algorithm without the alternating simulation loops for any possible search order.},
pdf ={http://www.cs.aau.dk/~srba/files/KLMS:PN:20.pdf},
ee ={https://link.springer.com/chapter/10.1007/978-3-030-51831-8_6},
doi ={10.1007/978-3-030-51831-8_6},
}

@inproceedings{BJLMS:CONCUR:19,
author ={F.M. B{\o}nneland and P.G. Jensen and K.G. Larsen and M. Muniz and J. Srba},
title ={Partial Order Reduction for Reachability Games},
booktitle ={Proceedings of the 30th International Conference on Concurrency Theory ({CONCUR}'19)},
year ={2019},
volume ={140},
series ={LIPICS},
pages ={23:1--23:15},
publisher ={Dagstuhl Publishing},
abstract ={Partial order reductions have been successfully applied to model checking of concurrent systems and practical applications of the technique show nontrivial reduction in the size of the explored state space. We present a theory of partial order reduction based on stubborn sets in the game-theoretical setting of 2-player games with reachability/safety objectives. Our stubborn reduction allows us to prune the interleaving behaviour of both players in the game, and we formally prove its correctness on the class of games played on general labelled transition systems. We then instantiate the framework to the class of weighted Petri net games with inhibitor arcs and provide its efficient implementation in the model checker TAPAAL. Finally, we evaluate our stubborn reduction on several case studies and demonstrate its efficiency.},
pdf ={http://www.cs.aau.dk/~srba/files/BJLMS:CONCUR:19.pdf},
doi ={10.4230/LIPIcs.CONCUR.2019.23},
ee ={https://drops.dagstuhl.de/opus/volltexte/2019/10925/},
note ={Please note that the paper contains an error that is fixed here: https://arxiv.org/abs/1912.09875},
}

@inproceedings{NLS:SPIN:19,
author ={S. Enevoldsen and K.G. Larsen and J. Srba},
title ={Model Verification Through Dependency Graphs},
booktitle ={Proceedings of the 26th International SPIN Symposium on Model Checking of Software ({SPIN}'19)},
year ={2019},
series ={LNCS},
volume ={11636},
pages ={1--19},
publisher ={Springer-Verlag},
abstract ={Dependency graphs, as introduced more than 20 years ago by Liu and Smolka, are oriented graphs with hyperedges that connect nodes with sets of target nodes in order to represent causal dependencies in the graph. Numerous verification problems can be reduced into the problem of computing a minimum or maximum fixed-point assignment on dependency graphs. In the original definition, assignments link each node with a Boolean value, however, in the recent work the assignment domains have been extended to more general setting, even including infinite domains. We present an overview of the recent results on extensions of dependency graphs in order to deal with verification of quantitative, probabilistic and timed systems.},
pdf ={http://www.cs.aau.dk/~srba/files/ELS:SPIN:19.pdf},
doi ={10.1007/978-3-030-30923-7_1},
ee ={https://link.springer.com/chapter/10.1007/978-3-030-30923-7_1},
}

@inproceedings{MCC:TACAS:19,
author ={E. Amparore and B. Berthomieu and G. Ciardo and S. Dal Zilio and F. Galla and M. Hillah and F. Hulin-Hubard and P.G. Jensen and L. Jezequel and F. Kordon and D. Le Botlan and T. Liebke and J. Meijer and A. Miner and E. Paviot-Adet and J. Srba and Y. Thierry-Mieg and T. van Dijk and K. Wolf},
title ={Presentation of the 9th Edition of the Model Checking Contest},
booktitle ={Proceedings of the 25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems ({TACAS}'19)},
year ={2019},
series ={LNCS},
volume ={11429},
publisher ={Springer-Verlag},
pages ={50--68},
abstract ={The Model Checking Contest (MCC) is an annual competition of software tools for model checking. Tools must process an increasing benchmark gathered from the whole community and may participate in various examinations: state space generation, computation of global properties, computation of some upper bounds in the model, evaluation of reachability formulas, evaluation of CTL formulas, and evaluation of LTL formulas.For each examination and each model instance, participating tools are provided with up to 3600 s and 16 gigabyte of memory. Then, tool answers are analyzed and confronted to the results produced by other competing tools to detect diverging answers (which are quite rare at this stage of the competition, and lead to penalties). For each examination, golden, silver, and bronze medals are attributed to the three best tools. CPU usage and memory consumption are reported, which is also valuable information for tool developers.},
pdf ={http://www.cs.aau.dk/~srba/files/MCC:TACAS:19.pdf},
doi ={10.1007/978-3-030-17502-3_4},
ee ={https://link.springer.com/chapter/10.1007%2F978-3-030-17502-3_4},
}

@inproceedings{KLLS:RSSRail:19,
author ={S.L. Karra and K.G. Larsen and F. Lorber and J. Srba},
title ={Safe and Time-Optimal Control for Railway Games},
booktitle ={Proceedings of International Conference on Reliability, Safety and Security of Railway Systems: Modelling, Analysis, Verification and Certification ({RSSRail}'19)},
year ={2019},
series ={LNCS},
volume ={11495},
publisher ={Springer-Verlag},
pages ={106--122},
abstract ={Railway scheduling is a complex and safety critical problem that has recently attracted attention in the formal verification community. We provide a formal model of railway scheduling as a stochastic timed game and using the tool Uppaal Stratego, we synthesise the most permissive control strategy for operating the lights and points at the railway scenario such that we guarantee system's safety (avoidance of train collisions). Among all such safe strategies, we then select (with the help of reinforcement learning) a concrete strategy that minimizes the time needed to move all trains to their target locations. This optimizes the speed and capacity of a railway system and advances the current state-of-the-art where the optimality criteria were not considered yet. We successfully demonstrate our approach on the models of two Danish railway stations, and discuss the applicability and scalability of our approach.},
pdf ={http://www.cs.aau.dk/~srba/files/KLLS:RSSRail:19.pdf},
doi ={10.1007/978-3-030-18744-6_7},
ee ={https://link.springer.com/chapter/10.1007%2F978-3-030-18744-6_7},
}

@inproceedings{ELS:TACAS:19,
author ={S. Enevoldsen and K.G. Larsen and J. Srba},
title ={Abstract Dependency Graphs and Their Application to Model Checking},
booktitle ={Proceedings of the 25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems ({TACAS}'19)},
year ={2019},
series ={LNCS},
volume ={11427},
publisher ={Springer-Verlag},
pages ={316--333},
abstract ={Dependency graphs, invented by Liu and Smolka in 1998, are oriented graphs with hyperedges that represent dependencies among the values of the vertices. Numerous model checking problems are reducible to a computation of the minimum fixed-point vertex assignment. Recent works successfully extended the assignments in dependency graphs from the Boolean domain into more general domains in order to speed up the fixed-point computation or to apply the formalism to a more general setting of e.g. weighted logics. All these extensions require separate correctness proofs of the fixed-point algorithm as well as a one-purpose implementation. We suggest the notion of abstract dependency graphs where the vertex assignment is defined over an abstract algebraic structure of Noetherian partial orders with the least element. We show that existing approaches are concrete instances of our general framework and provide an open-source C++ library that implements the abstract algorithm. We demonstrate that the performance of our generic implementation is comparable to, and sometimes even outperforms, dedicated special-purpose algorithms presented in the literature.},
pdf ={http://www.cs.aau.dk/~srba/files/ELS:TACAS:19.pdf},
doi ={10.1007/978-3-030-17462-0_18},
ee ={https://link.springer.com/chapter/10.1007%2F978-3-030-17462-0_18},
}

@inproceedings{JKMSST:coNEXT:18,
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},
pages ={217--227},
publisher ={ACM},
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 about 100,000 forwarding rules.},
pdf ={http://www.cs.aau.dk/~srba/files/JKMSST:coNEXT:18.pdf},
doi ={10.1145/3281411.3281432},
ee ={https://dl.acm.org/citation.cfm?id=3281432},
}

@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 ={1799--1807},
year ={2018},
publisher ={{IEEE}},
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},
ee ={https://ieeexplore.ieee.org/document/8486261},
doi ={10.1109/INFOCOM.2018.8486261},
}

@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{SPS:FAC:24,
title ={Measurement-Noise Filtering for Automatic Discovery of Flow Splitting Ratios in ISP Networks},
author ={M.K. Schou and I. Poese and J. Srba},
journal ={Formal Aspects of Computing},
year ={2024},
volume ={},
pages ={1--18},
publisher ={Elsevier},
abstract ={Network telemetry and analytics is essential for providing highly dependable services in modern computer networks. In particular, network flow analytics for ISP networks allows operators to inspect and reason about traffic patterns in their networks in order to react to anomalies. High performance network analytics systems are designed with scalability in mind, and can consequently only observe partial information about the network traffic. Still, they need to provide a holistic view of the traffic, including the distribution of different traffic flows on each link. It is impractical to monitor such fine-grained telemetry, and in large, heterogeneous networks it is often too complex and error-prone, if not impossible, to access and maintain all technical specifications and router-specific configurations needed to determine e.g. the load balancing weights used when traffic is split onto multiple paths. The ratios by which flows are split on the possible paths must be derived indirectly from the measured flow demands and link utilizations. Motivated by a case study provided by a major European ISP, we suggest an efficient method to estimate the flow splitting ratios. Our approach, based on quadratic linear programming, is scalable and achieves robustness to the measurement noise found in a typical network analytics deployment by filtering out certain constraints in the linear program. Finally, we implement an automated tool for estimating the flow splitting ratios and document its applicability on real data from the ISP.},
issn ={1433-299X},
doi ={10.1145/3700602},
ee ={https://dl.acm.org/doi/10.1145/3700602},
pdf ={http://www.cs.aau.dk/~srba/files/SPS:FAC:24.pdf},
}

@article{GLNNQRSZ:NAHS:24,
title ={Optimal Control Strategies for Stormwater Detention Ponds},
author ={M.A. Goorden and K.G. Larsen and J.E. Nielsen and T.D. Nielsen and W. Qian and M.R. Rasmussen and J. Srba and G. Zhao},
journal ={Nonlinear Analysis: Hybrid Systems},
year ={2024},
volume ={53},
pages ={1--15},
publisher ={Elsevier},
abstract ={Stormwater detention ponds are essential stormwater management solutions that regulate the urban catchment discharge towards streams. Their purposes are to reduce the hydraulic load to avoid stream erosion, as well as to minimize the degradation of the natural waterbody by direct discharge of pollutants. Currently, static controllers are widely implemented for detention pond outflow regulation in engineering practice, i.e., the outflow discharge is capped at a fixed value. Such a passive discharge setting fails to exploit the full potential of the overall water system, hence further improvements are needed. We apply formal methods to synthesize (i.e., derive automatically) optimal active controllers. We model the stormwater detention pond, including the urban catchment area and the rain forecasts with its uncertainty, as hybrid Markov decision processes. Subsequently, we use the tool Uppaal Stratego to synthesize using Q-learning a control strategy maximizing the retention time for pollutant sedimentation (optimality) while also minimizing the duration of emergency overflow in the detention pond (safety). These strategies are synthesized for both an off-line and on-line settings. Simulation results for an existing pond show that Uppaal Stratego can learn optimal strategies that significantly reduce emergency overflows. For off-line controllers, a scenario with low rain periods shows a 26% improvement of pollutant sedimentation with respect to static control, and a scenario with high rain periods shows a reduction of overflow probability of 10%-19% for static control to lower than 5%, while pollutant sedimentation has only declined by 7% compared to static-control. For on-line controllers, one scenario with heavy rain shows a 95% overflow duration reduction and a 29% pollutant sedimentation improvement compared to static control.},
issn ={1751-570X},
doi ={10.1016/j.nahs.2024.101504},
ee ={https://www.sciencedirect.com/science/article/pii/S1751570X24000414},
pdf ={http://www.cs.aau.dk/~srba/files/GLNNQRSZ:NAHS:24.pdf},
}

@article{JKMNST:FAC:23,
title ={Kaki: Efficient Concurrent Update Synthesis for {SDN}},
author ={N.S. Johansen and L.B. Kaer and A.L. Madsen and K.O. Nielsen and J. Srba and R.G. Tollund},
journal ={Formal Aspects of Computing},
year ={2023},
volume ={35(3)},
pages ={1--22},
publisher ={ACM},
abstract ={Modern computer networks based on the software-defined networking (SDN) paradigm are becoming increasingly complex and often require frequent configuration changes in order to react to traffic fluctuations. It is essential that forwarding policies are preserved not only before and after the configuration update but also at any moment during the inherently distributed execution of such an update. We present Kaki, a Petri game based tool for automatic synthesis of switch batches which can be updated in parallel without violating a given (regular) forwarding policy like waypointing or service chaining. Kaki guarantees to find the minimum number of concurrent batches and supports both splittable and nonsplittable flow forwarding. In order to achieve optimal performance, we introduce two novel optimisation techniques based on static analysis: decomposition into independent subproblems and identification of switches that can be collectively updated in the same batch. These techniques considerably improve the performance of our tool Kaki, relying on TAPAAL's verification engine for Petri games as its backend. Experiments on a large benchmark of real networks from the Internet Topology Zoo database demonstrate that Kaki outperforms the state-of-the-art tools Netstack and FLIP. Kaki computes concurrent update synthesis significantly faster than Netstack and compared to FLIP, it provides shorter (and provably optimal) concurrent update sequences at similar runtimes.},
issn ={0934-5043},
doi ={10.1145/3605952},
ee ={https://dl.acm.org/doi/10.1145/3605952},
pdf ={http://www.cs.aau.dk/~srba/files/JKMNST:FAC:23.pdf},
}

@article{HJLS:SCP:23,
title ={A Toolchain for Domestic Heat-Pump Control Using UPPAAL STRATEGO},
author ={I.R. Hasrat and P.G. Jensen and K.G. Larsen and J. Srba},
journal ={Science of Computer Programming},
volume ={230},
pages ={1--20},
year ={2023},
issn ={0167-6423},
publisher ={Elsevier},
abstract ={Heatpump-based floor-heating systems for domestic heating offer flexibility in energy consumption patterns, which can be utilized for reducing heating costs-in particular whenconsidering hour-based electricity prices. Such flexibility is hard to exploit via classicalModel Predictive Control (MPC), and in addition, MPC requires a priori calibration (i.e.,model identification) which is often costly and becomes outdated as the dynamics anduse of a building change. We solve these shortcomings by combining recent advancementsin stochastic model identification and automatic (near-)optimal controller synthesis. Ourmethod suggests an adaptive model-identification using the tool CTSM-R, and an efficientcontrol synthesis based on Q-learning for Euclidean Markov Decision Processes via UppaalStratego. This paper investigates three potential control strategy perspectives (i.e., fixed-target, target-band, and setbacks) to achieve energy efficiency in the heating system. Toexamine the performance of the suggested approaches, we demonstrate our method on anexperimental Danish family-house from the OpSys project. The results show that a fixed-target strategy offers up to a 39% reduction in heating cost while retaining comparablecomfort to a standard bang-bang controller. Even better, target-band and setbacks strategiesgain up to 46-49% energy cost savings. Furthermore, we show the flexibility of our methodby computing the Pareto-frontier that visualizes the cost/comfort tradeoff. Additionally,we discuss the applicability of Stratego for an old-fashioned binary-mode heat-pumpsystem and report significant cost savings (33%) as compared to the bang-bang controller.Moreover, we also present the performance analysis of Stratego against an industry-standard control strategy.},
doi ={10.1016/j.scico.2023.102987},
ee ={https://www.sciencedirect.com/science/article/pii/S0167642323000692},
pdf ={http://www.cs.aau.dk/~srba/files/HJLS:SPC:23.pdf},
}

@article{LMSS:SCP:23,
title ={{AllSynth:} A {BDD}-Based Approach for Network Update Synthesis},
author ={K.G. Larsen and A. Mariegaard and S. Schmid and J. Srba},
journal ={Science of Computer Programming},
volume ={230},
pages ={1--19},
year ={2023},
issn ={0167-6423},
publisher ={Elsevier},
abstract ={The increasingly stringent dependability requirements on communication networks as well as the need to render these networks more adaptive to improve performance, demand for more automated approaches to operate networks. We present AllSynth, a symbolic synthesis tool for updating communication networks in a provably correct and efficient manner. AllSynth automatically synthesizes network update schedules which transiently ensure a wide range of policy properties expressed using linear temporal logic (LTL). In particular, in contrast to existing approaches, AllSynth symbolically computes and compactly represents all feasible and cost-optimal solutions. At its heart, AllSynth relies on a novel parameterized use of binary decision diagrams (BDDs) which greatly improves performance. Indeed, AllSynth not only provides formal correctness guarantees and outperforms existing state-of-the-art tools in terms of generality, but also in terms of runtime as documented by experiments on a benchmark of real-world network topologies.},
doi ={10.1016/j.scico.2023.102992},
ee ={https://www.sciencedirect.com/science/article/pii/S0167642323000746},
pdf ={http://www.cs.aau.dk/~srba/files/LMSS:SCP:23.pdf},
}

@article{ZRLSNGWN:hydro:2023,
title ={Determine Stormwater Pond Geometrics and Hydraulics Using Remote Sensing Technologies: A Comparison between Airborne-{LiDAR} and {UAV}-Photogrammetry Field Validation against {RTK-GNSS}},
author ={G. Zhao and M.R. Rasmussen and K.G. Larsen and J. Srba and T.D. Nielsen and M. Goorden and W. Qian and J.E. Nielsen},
abstract ={Flow-regulated stormwater ponds providing safe outflow discharges prevail as the primary stormwater management tool for stream protections. Detailed pond geometries are essential metrics in pond monitoring technologies, which convert the point-based water level measurements to areal/volumetric ponding water estimations. Unlike labour-intensive surveys (e.g., RTK-GNSS or total stations), UAV-photogrammetry and airborne-LiDAR have been advocated as cost-effective alternatives to acquire high-quality datasets. In this paper, we compare the use of these two approaches for stormwater pond surveys. With reference to RTK-GNSS in-situ observations, we identify their geometric and hydraulic discrepancies based on six stormwater ponds from three aspects: (i) DEMs, (ii) stage-curves and (iii) outflow discharges. Three main findings are outlined: (i) for wet ponds where moisture environments are dominant, UAV-photogrammetry outperforms (infrared) airborne-LiDAR, where airborne-LiDAR yields 0.15-0.54 NSEoutflow, which is unacceptable; (ii) for dry ponds, UAV-photogrammetry obtains 0.88-0.89 NSEoutflow as poor vegetation penetrations; two correction methods (i.e., grass removal and shifted stage-curves) are proposed, indicating good alignment to RTK-GNSS observations and (iii) UAV-photogrammetry delivers <0.1 m resolution in outlining break-line features for stormwater pond structures. With significant economic advantages, the multi-UAV collaborative photogrammetry would address the shortcomings of a single UAV and thus pave the way for large urban catchment/watershed survey applications.},
journal ={Journal of Hydroinformatics},
volume ={25},
number ={4},
publisher ={IWA Publishing},
pages ={1256--1275},
year ={2023},
issn ={1464-7141},
doi ={10.2166/hydro.2023.178},
ee ={https://doi.org/10.2166/hydro.2023.178},
pdf ={https://vbn.aau.dk/ws/portalfiles/portal/545272952/jh0251256.pdf},
}

@article{BJPST:FI:23,
author ={A. Bilgram and P.G. Jensen and T. Pedersen and J. Srba and P.H. Taankvist},
title ={Methods for Efficient Unfolding of Colored Petri Nets},
journal ={Fundamenta Informaticae},
year ={2023},
volume ={189},
number ={3--4},
pages ={297-320},
publisher ={IOS Press},
abstract ={Colored Petri nets offer a compact and user friendly representation of the traditional P/T nets and colored nets with finite color ranges can be unfolded into the underlying P/T nets, however, at the expense of an exponential explosion in size. We present two novel techniques based on static analysis in order to reduce the size of unfolded colored nets. The first method identifies colors that behave equivalently and groups them into equivalence classes, potentially reducing the number of used colors. The second method overapproximates the sets of colors that can appear in places and excludes colors that can never be present in a given place. Both methods are complementary and the combined approach allows us to significantly reduce the size of multiple colored Petri nets from the Model Checking Contest benchmark. We compare the performance of our unfolder with state-of-the-art techniques implemented in the tools MCC, Spike and ITS-Tools, and while our approach is competitive w.r.t. unfolding time, it also outperforms the existing approaches both in the size of unfolded nets as well as in the number of answered model checking queries from the 2021 Model Checking Contest.},
pdf ={https://arxiv.org/pdf/2204.07039},
issn ={0169-2968},
ee ={https://fi.episciences.org/12398},
}

@article{DJJKMSST:TON:21,
author ={I. van Duijn and P.G. Jensen and J.S. Jensen and T.B. Kr{\o}gh and J.S. Madsen and S. Schmid and J. Srba and M.T. Thorgersen},
title ={Automata-Theoretic Approach to Verification of {MPLS} Networks under Link Failures},
journal ={IEEE/ACM Transactions on Networking},
year ={2022},
volume ={30},
number ={2},
publisher ={IEEE},
pages ={766--781},
abstract ={Future communication networks are expected to be highly automated, disburdening human operators of their most complex tasks. While the first powerful and automated network analysis tools are emerging, existing tools provide only 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 and 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 which feature fast rerouting mechanisms with label stacks. In particular, P-REX allows to reason about recursive backup tunnels, by supporting potentially infinite state spaces. As P-REX directly operates on the actual dataplane configuration, i.e., forwarding tables, it is well-suited for debugging. Our tool comes with an expressive query language based on regular expressions. We also report on an industrial case study and demonstrate that our tool can perform what-if reachability analyses on average in about 5 seconds for a 24-router network with over 250,000 MPLS forwarding rules. This is a significant improvement to an earlier prototype of our tool presented in the conference version of our paper where the verification took on average about 1 hour.},
pdf ={http://www.cs.aau.dk/~srba/files/DJJKMSST:TON:21.pdf},
ee ={https://ieeexplore.ieee.org/document/9619760},
doi ={10.1109/TNET.2021.3126572},
}

@article{ELS:STTT:21,
author ={S. Enevoldsen and K.G. Larsen and J. Srba},
title ={Extended Abstract Dependency Graphs},
journal ={International Journal on Software Tools for Technology Transfer (STTT)},
year ={2022},
volume ={24},
number ={},
publisher ={Springer-Verlag},
pages ={49--65},
abstract ={Dependency graphs, invented by Liu and Smolka in 1998, are oriented graphs with hyperedges that represent dependencies among the values of the vertices. Numerous model checking problems are reducible to a computation of the minimum fixed-point vertex assignment. Recent works successfully extended the assignments in dependency graphs from the Boolean domain into more general domains in order to speed up the fixed-point computation or to apply the formalism to a more general setting of, for example, weighted logics. All these extensions require separate correctness proofs of the fixed-point algorithm as well as a one-purpose implementation. We suggest the notion of extended abstract dependency graphs where the vertex assignment is defined over an abstract algebraic structure of Noetherian partial orders with the least element, and where we allow both monotonic and non-monotonic functions. We show that existing approaches are concrete instances of our general framework and provide an open-source C++ library that implements the abstract algorithm. We demonstrate that the performance of our generic implementation is comparable to, and sometimes even outperforms, dedicated special-purpose algorithms presented in the literature.},
pdf ={http://www.cs.aau.dk/~srba/files/ELS:STTT:21.pdf},
ee ={https://link.springer.com/article/10.1007/s10009-021-00638-8},
doi ={10.1007/s10009-021-00638-8},
}

@article{BJLMS:LMCS:21,
author ={F.M. B{\o}nneland and P.G. Jensen and K.G. Larsen and M. Muniz and J. Srba},
title ={Stubborn Set Reduction for Two-Player Reachability Games},
journal ={Logical Methods in Computer Science},
publisher ={Creative Commons},
volume ={17},
number ={1},
pages ={1--26},
year ={2021},
abstract ={Partial order reductions have been successfully applied to model checking of concurrent systems and practical applications of the technique show nontrivial reduction in the size of the explored state space. We present a theory of partial order reduction based on stubborn sets in the game-theoretical setting of 2-player games with reachability objectives. Our stubborn reduction allows us to prune the interleaving behaviour of both players in the game, and we formally prove its correctness on the class of games played on general labelled transition systems. We then instantiate the framework to the class of weighted Petri net games with inhibitor arcs and provide its efficient implementation in the model checker TAPAAL. Finally, we evaluate our stubborn reduction on several case studies and demonstrate its efficiency.},
ee ={https://lmcs.episciences.org/7278/},
pdf ={https://arxiv.org/abs/1912.09875v7},
}

@article{ELMS:STTT:20,
author ={S. Enevoldsen and K.G. Larsen and A. Mariegaard and J. Srba},
title ={Dependency Graphs with Applications to Verification},
journal ={International Journal on Software Tools for Technology Transfer (STTT)},
year ={2020},
volume ={22},
publisher ={Springer-Verlag},
pages ={635--654},
abstract ={Dependency graphs, as introduced more than 20 years ago by Liu and Smolka, are oriented graphs with hyperedges that connect nodes with sets of target nodes in order to represent causal dependencies in the graph. Numerous verification problems can be reduced into the problem of computing a minimum or maximum fixed-point assignment on dependency graphs. In the original definition, assignments link each node with a Boolean value, however, in the recent work the assignment domains have been extended to more general setting, even including infinite domains. In this survey paper, we present an overview of the recent results on extensions of dependency graphs in order to deal with verification of quantitative, probabilistic, parameterized and timed systems.},
pdf ={http://www.cs.aau.dk/~srba/files/ELMS:STTT:20.pdf},
ee ={https://link.springer.com/article/10.1007/s10009-020-00578-9},
doi ={10.1007/s10009-020-00578-9},
}

@article{JKLNS:JLAMP:19,
author ={J.S. Jensen and I. Kaufmann and K.G. Larsen and S.M. Nielsen and J. Srba},
title ={Model Checking and Synthesis for Branching Multi-Weighted Logics},
journal ={Journal of Logical and Algebraic Methods in Programming},
year ={2019},
volume ={105},
number ={1},
pages ={28--46},
publisher ={Elsevier},
abstract ={We investigate the open synthesis problem in a quantitative game theoretic setting where the system model is annotated with multiple nonnegative weights representing quantitative resources such as energy, discrete time or cost. We consider system specifications expressed in the branching time logic CTL extended with bounds on resources. As our first contribution, we show that the model checking problem for the full logic is undecidable with already three weights. By restricting the bounds to constant upper or lower-bounds on the individual weights, we demonstrate that the problem becomes decidable and that the model checking problem is PSPACE-complete. As a second contribution, we show that by imposing upper-bounds on the temporal operators and assuming that the cost converges over infinite runs, the synthesis problem is also decidable. Finally, we provide an on-the-fly algorithm for the synthesis problem on an unrestricted model for a reachability fragment of the logic and we prove EXPTIME-completeness of the synthesis problem.},
doi ={10.1016/j.jlamp.2019.02.001},
ee ={https://www.sciencedirect.com/science/article/pii/S2352220818300336?via%3Dihub},
pdf ={http://www.cs.aau.dk/~srba/files/JKLNS:JLAMP:19.pdf},
}

@article{BDJJS:JLAMP:19,
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 ={2019},
volume ={102},
number ={1},
pages ={46--63},
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.},
pdf ={http://www.cs.aau.dk/~srba/files/BDJJS:JLAMP:19.pdf},
doi ={10.1016/j.jlamp.2018.09.002},
ee ={https://www.sciencedirect.com/science/article/pii/S235222081830035X?via%3Dihub},
}

@article{TPNOMOC:18,
author ={F. Kordon and H. Garavel and L.-M. Hillah and E. Paviot-Adet and L. Jezequel and F. Hulin-Hubard and E.G. Amparore and M. Beccuti and B. Berthomieu and H. Evrard and P.G. Jensen and D. Le Botlan and T. Liebke and J. Meijer and J. Srba and Y. Thierry-Mieg and J. van de Pol and K. Wolf},
title ={MCC'2017 - The Seventh Model Checking Contest},
journal ={T. Petri Nets and Other Models of Concurrency},
year ={2018},
volume ={13},
pages ={181--209},
publisher ={Springer},
abstract ={Created in 2011, the Model Checking Contest (MCC) is an annualcompetition dedicated to provide a fair evaluation of software tools thatverify concurrent systems using state-space exploration techniques andmodel checking. This article presents the principles and results of the2017 edition of the MCC, which took place along with the Petri Net andACSD joint conferences in Zaragoza, Spain.},
pdf ={http://www.cs.aau.dk/~srba/files/TPNOMOC:18.pdf},
doi ={10.1007/978-3-662-58381-4_9},
ee ={https://link.springer.com/chapter/10.1007%2F978-3-662-58381-4_9},
}

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

@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:19,
title ={Selected papers from the 28th Nordic Workshop on Programming Theory ({NWPT}'16)},
author ={K.G. Larsen and J. Srba},
journal ={Journal of Logical and Algebraic Methods in Programming},
volume ={107},
pages ={177--178},
year ={2019},
issn ={2352-2208},
doi ={https://doi.org/10.1016/j.jlamp.2019.07.002},
ee ={http://www.sciencedirect.com/science/article/pii/S2352220819300896},
}

@proceedings{LPS:TCS:18,
author ={K.G. Larsen and I. Potapov and J. Srba},
title ={Reachability Problems: Special Issue},
journal ={Theoretical Computer Science},
year ={2018},
ee ={https://www.sciencedirect.com/journal/theoretical-computer-science/vol/750/suppl/C},
}

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