Abstract We introduce a formal modeling methodology to analyze quantum communication protocols in the tool Uppaal . Our approach encodes quantum states, operations, and measurements into Uppaal timed automata with data extensions and external function calls, enabling both exhaustive verification in the ideal (noiseless) case and statistical model checking for realistic noisy scenarios. We apply our framework to the Beyond Superdense Coding protocol—a time-slotted variant of superdense coding—combined with quantum entanglement distillation, and demonstrate that Uppaal can deal with these protocols even under complex timing and decoherence constraints.

International audience

Dependency graphs have emerged as a versatile and powerful formalism with wide-ranging applications in formal verification. In this extended abstract, we provide an overview of selected advancements in on-the-fly verification techniques based on dependency graphs, focusing on the recent developments, optimizations and generalizations of this generic verification framework.

Effective scheduling of software updates is a significant challenge in network operations and management, particularly when considering specific performance and security requirements. This paper focuses on the synthesis of such software updates in the context of emerging virtualized and softwarized networks, such as 5G network infrastructures, with the objective of ensuring vulnerability avoidance and congestion freedom at any time during the updates. We formalize the update synthesis problem and propose an algorithmic solution, called Eagle, that exploits formal methods and mixed integer linear programming, to achieve optimal solutions. We then complement it with a greedy algorithm to support faster computation. We exemplify our framework considering an implementation of a 5G architecture, as the one described in the ETSI 5123 standard, and which relies on kubernetes. Finally, we evaluate our approach through a large range of realistic ISP topologies from the Topology Zoo dataset, and we also perform extensive experiments on our kubernetes cluster, where we execute the software update sequences generated by our tool. This allows us to discuss the scalability of our approach along with its practical applicability.

To achieve fast recovery from link failures, most modern communication networks feature fully decentralized fast re-routing mechanisms. These re-routing mechanisms rely on pre-installed static re-routing rules at the nodes (the routers), which depend only on local failure information, namely on the failed links incident to the node. Ideally, a network is perfectly resilient: the re-routing rules ensure that packets are always successfully routed to their destinations as long as the source and the destination are still physically connected in the underlying network after the failures. Unfortunately, there are examples where achieving perfect resilience is not possible. Surprisingly, only very little is known about the algorithmic aspect of when and how perfect resilience can be achieved. We investigate the computational complexity of analyzing such local fast re-routing mechanisms. Our main result is a negative one: we show that even checking whether a given set of static re-routing rules ensures perfect resilience is coNP-complete. Additionally, we investigate other fundamental variations of the problem. In particular, we show that our coNP-completeness proof also applies to scenarios where the re-routing rules have specific patterns (known as skipping in the literature). On the positive side, for scenarios where nodes do not have information about the link from which a packet arrived (the so-called in-port), we present a linear-time algorithm to realize perfect resilience whenever possible (which we show can also be determined in linear time).

Abstract We propose a novel state-space reduction framework to improve the performance of model checking of Petri nets. We provide two instances of the framework: a static technique that considers only the structure of the net, and a dynamic technique that additionally considers the current marking. By analyzing impossible, visible, and directional effects of transitions, we identify places where tokens can be removed while preserving the property in question. Unlike structural reductions, our techniques modify only the current marking, allowing the net structure to be reused in multiple subproblems concurrently, which can be beneficial for example for CTL model checking. We prove the correctness of our techniques and implement them in the open-source tool Tapaal, a repeated winner in the CTL category in the annual model checking contest (MCC). We measure our methods’ performance on the MCC 2023 benchmark using the CTL categories and demonstrate that our methods reduce time and, especially, memory usage. Our dynamic method explores 39.3% fewer configurations on average and achieves two orders of magnitude speedup on at least one query on 23.7% of non-trivial models.

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.

Modern communication networks support local fast re-routing (FRR) to quickly react to link failures. However, configuring such FRR mechanisms is challenging as the rules have 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 present a 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.

Network telemetry and analytics is essential for providing highly dependable services in modern computer networks. In particular, network flow analytics for internet service provider (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, for example, 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.

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.

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.

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. This paper investigates three potential control strategy perspectives (i.e., fixed-target, target-band, and setbacks) to achieve energy efficiency in the heating system. To examine the performance of the suggested approaches, we demonstrate our method on an experimental 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 comparable comfort to a standard bang-bang controller. Even better, target-band and setbacks strategies gain up to 46-49 % energy cost savings. Furthermore, we show the flexibility of our method by computing the Pareto-frontier that visualizes the cost/comfort tradeoff. Additionally, we discuss the applicability of Stratego for an old-fashioned binary-mode heat-pump system 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.

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.

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

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.

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.

Colored Petri nets offer a compact and user friendly representation of the traditional Place/Transition (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.

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 aboutfailure scenarios. We present P-REX, a fastwhat-if analysistool, that allows us to test important reachability and policy-compliance properties even under anarbitrary numberof failures and inpolynomial-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.

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 alongfeasiblepaths, without violating capacity constraints, for up toklink 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: apessimisticmodel where flows interfere in a worst-case manner along equal-cost shortest paths, and anoptimisticmodel 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.

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.

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.

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.

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.

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.

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 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, 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 over 100,000 MPLS forwarding rules.

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.

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 t o 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.

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

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.

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 first consider the discrete-time semantics (integer delays) and explore the decidability of the soundness 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. We also discuss the soundness problem in the continuous-time semantics (real-number delays) and show that for nets with nonstrict guards (where the reachability question coincides for both semantics) the soundness checking problem does not in general follow the approach for the discrete semantics and different zone-based techniques are needed for introducing its decidability in the bounded case. 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 (www.tapaal.net).

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.

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 system developers to employ more complex label refinement than in 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, determinisation, parallel composition, conjunction, quotient and logical characterisation of label-structured modal transition systems.

Stirling [1996, 1998] proved the decidability of bisimilarity on so-called normed pushdown processes. This result was substantially extended by Sénizergues [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 ε -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 ε -popping pushdown processes, was left open. This was repeatedly indicated by both Stirling and Sénizergues. 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 Π 0 1 -complete or Σ 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 Σ 1 1 -complete. Third, we show Σ 1 1 -completeness of weak bisimilarity for so-called parallel pushdown (or multiset) automata, a subclass of (labeled, place/transition) Petri nets.

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 -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 also consider 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.

We define a class of transition systems called effective commutative transition systems (ECTS) and show, by generalising a tableaubased 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.