We study timed systems in which some timing features are unknown parameters. Parametric timed automata (PTAs) are a classical formalism for such systems but for which most interesting problems are undecidable. Notably, the parametric reachability emptiness problem, i.e., the emptiness of the parameter valuations set allowing to reach some given discrete state, is undecidable. Lower-bound/upper-bound parametric timed automata (L/U-PTAs) achieve decidability for reachability properties by enforcing a separation of parameters used as upper bounds in the automaton constraints, and those used as lower bounds.
In this paper, we first study reachability. We exhibit a subclass of PTAs (namely integer-points PTAs) with bounded rational-valued parameters for which the parametric reachability emptiness problem is decidable. Using this class, we present further results improving the boundary between decidability and undecidability for PTAs and their subclasses such as L/U-PTAs.
We then study liveness. We prove that:
(1) deciding the existence of at least one parameter valuation for which there exists an infinite run in an L/U-PTA is PSpace-complete;
(2) the existence of a parameter valuation such that the system has a deadlock is however undecidable;
(3) the problem of the existence of a valuation for which a run remains in a given set of locations exhibits a very thin border between decidability and undecidability.
We consider the model checking problem of infinite state systems given in the form of parameterized discrete timed networks with multiple clocks. We show that this problem is decidable with respect to specifications given by B- or S-automata. Such specifications are very expressive (they strictly subsume omega-regular specifications), and easily express complex liveness and safety properties. Our results are obtained by modeling the passage of time using symmetric broadcast, and by solving the model checking problem of parameterized systems of un-timed processes communicating using k-wise rend…
We revisit a fundamental result in real-time verification, namely that the binary reachability relation between configurations of a given timed automaton is definable in linear arithmetic over the integers and reals. In this paper we give a new and simpler proof of this result, building on the well-known reachability analysis of timed automata involving difference bound matrices. Using this new proof, we give an exponential-space procedure for model checking the reachability fragment of the logic parametric TCTL. Finally we show that the latter problem is NEXPTIME-hard.
Backwards reachability is an efficient zone-based approach for model checking probabilistic timed automata w.r.t. PTCTL properties. Current implementations, however, are restricted to maximum probabilities of reachability properties. In this paper, we report on our new implementation of backwards reachability as part of the Modest Toolset. Its support for minimum and maximum probabilities of until formulas makes it the most general implementation available today. We compare its behaviour to the experimental results reported in the original papers presenting the backwards reachability technique…
We consider pushdown timed automata (PTAs) that are timed automata (with dense clocks) augmented with a pushdown stack. A configuration of a PTA includes a control state, dense clock values and a stack word. By using the pattern technique, we give a decidable characterization of the binary reachability (i.e., the set of all pairs of configurations such that one can reach the other) of a PTA. Since a timed automaton can be treated as a PTA without the pushdown stack, we can show that the binary reachability of a timed automaton is definable in the additive theory of reals and integers. The resu…
Weighted timed automata have been defined in the early 2000's for modelling resource-consumption or -allocation problems in real-time systems. Optimal reachability is decidable in weighted timed automata, and a symbolic forward algorithm has been developed to solve that problem. This algorithm uses so-called priced zones, an extension of standard zones with cost functions. In order to ensure termination, the algorithm requires clocks to be bounded. For unpriced timed automata, much work has been done to develop sound abstractions adapted to the forward exploration of timed automata, ensuring t…
We show that it is decidable whether a transitive mixed linear relation has an $ω$-chain. Using this result, we study a number of liveness verification problems for generalized timed automata within a unified framework. More precisely, we prove that (1) the mixed linear liveness problem for a timed automaton with dense clocks, reversal-bounded counters, and a free counter is decidable, and (2) the Presburger liveness problem for a timed automaton with discrete clocks, reversal-bounded counters, and a pushdown stack is decidable.
We study the reachability problem for communicating timed processes, both in discrete and dense time. Our model comprises automata with local timing constraints communicating over unbounded FIFO channels. Each automaton can only access its set of local clocks; all clocks evolve at the same rate. Our main contribution is a complete characterization of decidable and undecidable communication topologies, for both discrete and dense time. We also obtain complexity results, by showing that communicating timed processes are at least as hard as Petri nets; in the discrete time, we also show equivalen…
Place/transition Petri nets are a standard model for a class of distributed systems whose reachability spaces might be infinite. One of well-studied topics is the verification of safety and liveness properties in this model; despite the extensive research effort, some basic problems remain open, which is exemplified by the open complexity status of the reachability problem. The liveness problems are known to be closely related to the reachability problem, and many structural properties of nets that are related to liveness have been studied. Somewhat surprisingly, the decidability status of the…
We consider Dense-Timed Petri Nets (TPN), an extension of Petri nets in which each token is equipped with a real-valued clock and where the semantics is lazy (i.e., enabled transitions need not fire; time can pass and disable transitions). We consider the following verification problems for TPNs. (i) Zenoness: whether there exists a zeno-computation from a given marking, i.e., an infinite computation which takes only a finite amount of time. We show decidability of zenoness for TPNs, thus solving an open problem from [Escrig et al.]. Furthermore, the related question if there exist arbitrarily…
We consider the reachability problem for timed automata having diagonal constraints (like x - y < 5) as guards in transitions. The best algorithms for timed automata proceed by enumerating reachable sets of its configurations, stored in the form of a data structure called "zones". Simulation relations between zones are essential to ensure termination and efficiency. The algorithm employs a simulation test "is-Z-simulated-by-Z' ?" which ascertains that zone Z does not reach more states than zone Z', and hence further enumeration from Z is not necessary. No effective simulations are known for ti…
Standard algorithms for reachability analysis of timed automata are sensitive to the order in which the transitions of the automata are taken. To tackle this problem, we propose a ranking system and a waiting strategy. This paper discusses the reason why the search order matters and shows how a ranking system and a waiting strategy can be integrated into the standard reachability algorithm to alleviate and prevent the problem respectively. Experiments show that the combination of the two approaches gives optimal search order on standard benchmarks except for one example. This suggests that it …
We study an expressive model of timed pushdown automata extended with modular and fractional clock constraints. We show that the binary reachability relation is effectively expressible in hybrid linear arithmetic with a rational and an integer sort. This subsumes analogous expressibility results previously known for finite and pushdown timed automata with untimed stack. As key technical tools, we use quantifier elimination for a fragment of hybrid linear arithmetic and for cyclic order atoms, and a reduction to register pushdown automata over cyclic order atoms.
Stochastic timed games (STGs), introduced by Bouyer and Forejt, naturally generalize both continuous-time Markov chains and timed automata by providing a partition of the locations between those controlled by two players (Player Box and Player Diamond) with competing objectives and those governed by stochastic laws. Depending on the number of players---$2$, $1$, or $0$---subclasses of stochastic timed games are often classified as $2\frac{1}{2}$-player, $1\frac{1}{2}$-player, and $\frac{1}{2}$-player games where the $\frac{1}{2}$ symbolizes the presence of the stochastic "nature" player. For S…
Given the versatility of timed automata a huge body of work has evolved that considers extensions of timed automata. One extension that has received a lot of interest is timed automata with a, possibly unbounded, stack, also called the pushdown timed automata (PDTA) model. While different algorithms have been given for reachability in different variants of this model, most of these results are purely theoretical and do not give rise to efficient implementations. One main reason for this is that none of these algorithms (and the implementations that exist) use the so-called zone-based abstracti…
Timed pushdown automata (TPDA) are an expressive formalism combining recursion with a rich logic of timing constraints. We prove that reachability relations of TPDA are expressible in linear arithmetic, a rich logic generalising Presburger arithmetic and rational arithmetic. The main technical ingredients are a novel quantifier elimination result for clock constraints (used to simplify the syntax of TPDA transitions), the use of clock difference relations to express reachability relations of the fractional clock values, and an application of Parikh's theorem to reconstruct the integral clock v…
In a reachability-time game, players Min and Max choose moves so that the time to reach a final state in a timed automaton is minimised or maximised, respectively. Asarin and Maler showed decidability of reachability-time games on strongly non-Zeno timed automata using a value iteration algorithm. This paper complements their work by providing a strategy improvement algorithm for the problem. It also generalizes their decidability result because the proposed strategy improvement algorithm solves reachability-time games on all timed automata. The exact computational complexity of solving reacha…
We study reachability games on recursive timed automata (RTA) that generalize Alur-Dill timed automata with recursive procedure invocation mechanism similar to recursive state machines. It is known that deciding the winner in reachability games on RTA is undecidable for automata with two or more clocks, while the problem is decidable for automata with only one clock. Ouaknine and Worrell recently proposed a time-bounded theory of real-time verification by claiming that restriction to bounded-time recovers decidability for several key decision problem related to real-time verification. We revis…
Updatable timed automata (UTA) are extensions of classic timed automata that allow special updates to clock variables, like x:= x - 1, x := y + 2, etc., on transitions. Reachability for UTA is undecidable in general. Various subclasses with decidable reachability have been studied. A generic approach to UTA reachability consists of two phases: first, a static analysis of the automaton is performed to compute a set of clock constraints at each state; in the second phase, reachable sets of configurations, called zones, are enumerated. In this work, we improve the algorithm for the static analysi…
Interrupt Timed Automata (ITA) is an expressive timed model, introduced to take into account interruptions, according to levels. Due to this feature, this formalism is incomparable with Timed Automata. However several decidability results related to reachability and model checking have been obtained. We add auxiliary clocks to ITA, thereby extending its expressive power while preserving decidability of reachability. Moreover, we define a parametrized version of ITA, with polynomials of parameters appearing in guards and updates. While parametric reasoning is particularly relevant for timed mod…
Counter systems are a well-known and powerful modeling notation for specifying infinite-state systems. In this paper we target the problem of checking temporal properties of counter systems. We first focus on checking liveness properties only, and propose two semi decision techniques for these properties. Both these techniques return a formula that encodes the set of reachable states of a given system that satisfy a given liveness property. A novel aspect of our techniques is that they use reachability analysis techniques, which are well studied in the literature, as black boxes, and are hence…
Timed-arc Petri nets (TAPN) are a well-known time extension of the Petri net model and several translations to networks of timed automata have been proposed for this model. We present a direct, DBM-based algorithm 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-space reduction technique introducing a monotonic ordering on markings and prove its soundness ev…
Model checkers for timed automata are widely used to verify safety-critical, real-time systems. State-of-the-art tools achieve scalability by intricate abstractions. We aim at further increasing the trust in their verification results, in particular for checking liveness properties. To this end, we develop an approach for extracting certificates for the emptiness of timed Büchi automata from model checking runs. These certificates can be double-checked by a certifier that we formally verify in Isabelle/HOL. We study liveness certificates in an abstract setting and show that our approach is sou…
Parametric timed automata (PTA) are an extension of timed automata in which clocks can be compared against parameters. The reachability problem asks for the existence of an assignment of the parameters to the non-negative integers such that reachability holds in the underlying timed automaton. The reachability problem for PTA is long known to be undecidable, already over three parametric clocks. A few years ago, Bundala and Ouaknine proved that for PTA over two parametric clocks and one parameter the reachability problem is decidable and also showed a lower bound for the complexity class PSPAC…
I/O conformance testing theories (e.g., ioco) are concerned with formally defining when observable output behaviors of an implementation conform to those permitted by a specification. Thereupon, several real-time extensions of ioco, usually called tioco, have been proposed, further taking into account permitted delays between actions. In this paper, we propose an improved version of tioco, called live timed ioco (ltioco), tackling various weaknesses of existing definitions. Here, a reasonable adaptation of quiescence (i.e., observable absence of any outputs) to real-time behaviors has to be do…
The timed automata formalism is an important model for specifying and analysing real-time systems. Robustness is the correctness of the model in the presence of small drifts on clocks or imprecision in testing guards. A symbolic algorithm for the analysis of the robustness of timed automata has been implemented. In this paper, we re-analyse an industrial case lip synchronization protocol using the new robust reachability algorithm. This lip synchronization protocol is an interesting case because timing aspects are crucial for the correctness of the protocol. Several versions of the model are c…
Probabilistic timed automata are a suitable formalism to model systems with real-time, nondeterministic and probabilistic behaviour. We study two-player zero-sum games on such automata where the objective of the game is specified as the expected time to reach a target. The two players---called player Min and player Max---compete by proposing timed moves simultaneously and the move with a shorter delay is performed. The first player attempts to minimise the given objective while the second tries to maximise the objective. We observe that these games are not determined, and study decision proble…
In this paper we consider state reachability in networks composed of many identical processes running a parametric timed broadcast protocol (PTBP). PTBP are a new model extending both broadcast protocols and parametric timed automata. This work is, up to our knowledge, the first to consider the combination of both a parametric network size and timing parameters in clock guard constraints. Since the communication topology is of utmost importance in broadcast protocols, we investigate reachability problems in both clique semantics where every message reaches every processes, and in reconfigurabl…
We study decidability of verification problems for timed automata extended with unbounded discrete data structures. More detailed, we extend timed automata with a pushdown stack. In this way, we obtain a strong model that may for instance be used to model real-time programs with procedure calls. It is long known that the reachability problem for this model is decidable. The goal of this paper is to identify subclasses of timed pushdown automata for which the language inclusion problem and related problems are decidable.
We study the verification of a finite continuous-time Markov chain (CTMC) C against a linear real-time specification given as a deterministic timed automaton (DTA) A with finite or Muller acceptance conditions. The central question that we address is: what is the probability of the set of paths of C that are accepted by A, i.e., the likelihood that C satisfies A? It is shown that under finite acceptance criteria this equals the reachability probability in a finite piecewise deterministic Markov process (PDP), whereas for Muller acceptance criteria it coincides with the reachability probability…
Parametric timed automata (PTA) extend timed automata by allowing parameters in clock constraints. Such a formalism is for instance useful when reasoning about unknown delays in a timed system. Using existing techniques, a user can synthesize the parameter constraints that allow the system to reach a specified goal location, regardless of how much time has passed for the internal clocks. We focus on synthesizing parameters such that not only the goal location is reached, but we also address the following questions: what is the minimal time to reach the goal location? and for which parameter va…
Timed automata have been introduced by Rajeev Alur and David Dill in the early 90's. In the last decades, timed automata have become the de facto model for the verification of real-time systems. Algorithms for timed automata are based on the traversal of their state-space using zones as a symbolic representation. Since the state-space is infinite, termination relies on finite abstractions that yield a finite representation of the reachable states. The first solution to get finite abstractions was based on extrapolations of zones, and has been implemented in the industry-strength tool Uppaal. A…
We consider the reachability problem for timed automata. A standard solution to this problem involves computing a search tree whose nodes are abstractions of zones. These abstractions preserve underlying simulation relations on the state space of the automaton. For both effectiveness and efficiency reasons, they are parametrized by the maximal lower and upper bounds (LU-bounds) occurring in the guards of the automaton. We consider the aLU abstraction defined by Behrmann et al. Since this abstraction can potentially yield non-convex sets, it has not been used in implementations. We prove that a…
Witnessing subsystems have proven to be a useful concept in the analysis of probabilistic systems, for example as diagnostic information on why a given property holds or as input to refinement algorithms. This paper introduces witnessing subsystems for reachability problems in probabilistic timed automata (PTA). Using a new operation on difference bounds matrices, it is shown how Farkas certificates of finite-state bisimulation quotients of a PTA can be translated into witnessing subsystems. We present algorithms for the computation of minimal witnessing subsystems under three notions of minim…
Parametric timed automata are a powerful formalism for reasoning on concurrent real-time systems with unknown or uncertain timing constants. In order to test the efficiency of new algorithms, a fair set of benchmarks is required. We present an extension of the IMITATOR benchmarks library, that accumulated over the years a number of case studies from academic and industrial contexts. We extend here the library with several dozens of new benchmarks; these benchmarks highlight several new features: liveness properties, extensions of (parametric) timed automata (including stopwatches or multi-rate…
Motivated by the success of bounded model checking framework for finite state machines, Ouaknine and Worrell proposed a time-bounded theory of real-time verification by claiming that restriction to bounded-time recovers decidability for several key decision problem related to real-time verification. In support of this theory, the list of undecidable problems recently shown decidable under time-bounded restriction is rather impressive: language inclusion for timed automata, emptiness problem for alternating timed automata, and emptiness problem for rectangular hybrid automata. The objective of …
Dense Integer-Complete Synthesis for Bounded Parametric Timed Automata
Université Sorbonne Paris Nord（索邦巴黎北大学）；Institut Universitaire de France (IUF)（法国大学研究院）；Nantes Université, École Centrale Nantes, CNRS, LS2N（南特大学，中央理工-南特学院，法国国家科学研究中心，LS2N）
We consider the reachability problem for timed automata. A standard solution to this problem involves computing a search tree whose nodes are abstractions of zones. For efficiency reasons, they are parametrized by the maximal lower and upper bounds (LU-bounds) occurring in the guards of the automaton. We propose an algorithm that is updating LU-bounds during exploration of the search tree. In order to keep them as small as possible, the bounds are refined only when they enable a transition that is impossible in the unabstracted system. So our algorithm can be seen as a kind of lazy CEGAR algor…
In this tutorial, we illustrate through examples how we can combine two classical models, namely those of pushdown automata (PDA) and timed automata, in order to obtain timed pushdown automata (TPDA). Furthermore, we describe how the reachability problem for TPDAs can be reduced to the reachability problem for PDAs.
This paper investigates the time-bounded version of the reachability problem for hybrid automata. This problem asks whether a given hybrid automaton can reach a given target location within T time units, where T is a constant rational value. We show that, in contrast to the classical (unbounded) reachability problem, the timed-bounded version is decidable for rectangular hybrid automata provided only non-negative rates are allowed. This class of systems is of practical interest and subsumes, among others, the class of stopwatch automata. We also show that the problem becomes undecidable if eit…
We consider the model of parametrized asynchronous shared-memory pushdown systems, as introduced in [Hague'11]. In a series of recent papers it has been shown that reachability in this model is PSPACE-complete [Esparza, Ganty, Majumdar'13] and that liveness is decidable in NEXPTIME [Durand-Gasselin, Esparza, Ganty, Majumdar'15]. We show here that the liveness problem is PSPACE-complete. We also introduce the universal reachability problem. We show that it is decidable, and coNEXPTIME-complete. Finally, using these results, we prove that the verifying regular properties of traces of executions,…
In this paper, we study thetime-bounded reachability problem for rectangular hybrid automata with non-negative rates (RHA+). This problem was recently shown to be decidable [Brihaye et al, ICALP11] (even though the unbounded reachability problem for even very simple classes of hybrid automata is well-known to be undecidable). However, [Brihaye et al, ICALP11] does not provide a precise characterisation of the complexity of the time-bounded reachability problem. The contribution of the present paper is threefold. First, we provide a new NExpTime algorithm to solve the timed-bounded reachability…
A popular method for solving reachability in timed automata proceeds by enumerating reachable sets of valuations represented as zones. A naïve enumeration of zones does not terminate. Various termination mechanisms have been studied over the years. Coming up with efficient termination mechanisms has been remarkably more challenging when the automaton has diagonal constraints in guards. In this paper, we propose a new termination mechanism for timed automata with diagonal constraints based on a new simulation relation between zones. Experiments with an implementation of this simulation show sig…
Markov automata combine non-determinism, probabilistic branching, and exponentially distributed delays. This compositional variant of continuous-time Markov decision processes is used in reliability engineering, performance evaluation and stochastic scheduling. Their verification so far focused on single objectives such as (timed) reachability, and expected costs. In practice, often the objectives are mutually dependent and the aim is to reveal trade-offs. We present algorithms to analyze several objectives simultaneously and approximate Pareto curves. This includes, e.g., several (timed) reac…
Markov automata (MAs) extend labelled transition systems with random delays and probabilistic branching. Action-labelled transitions are instantaneous and yield a distribution over states, whereas timed transitions impose a random delay governed by an exponential distribution. MAs are thus a nondeterministic variation of continuous-time Markov chains. MAs are compositional and are used to provide a semantics for engineering frameworks such as (dynamic) fault trees, (generalised) stochastic Petri nets, and the Architecture Analysis & Design Language (AADL). This paper considers the quantitative…
Although decidable, the marking reachability problem for Petri nets is well-known to be intractable in general, and a non-elementary lower bound has been recently uncovered. In order to alleviate this difficulty, various structural and behavioral restrictions have been considered, allowing to relate reachability to properties that are easier to check. For a given initial marking, the set of potentially reachable markings is described by the state equation solutions and over-approximates the set of reachable markings. In this paper, we delineate several subclasses of weighted Petri nets in whic…
We consider the problem of verifying liveness for systems with a finite, but unbounded, number of processes, commonly known as parameterised systems. Typical examples of such systems include distributed protocols (e.g. for the dining philosopher problem). Unlike the case of verifying safety, proving liveness is still considered extremely challenging, especially in the presence of randomness in the system. In this paper we consider liveness under arbitrary (including unfair) schedulers, which is often considered a desirable property in the literature of self-stabilising systems. We introduce an…
The parameter synthesis problem for parametric timed automata is undecidable in general even for very simple reachability properties. In this paper we introduce restrictions on parameter valuations under which the parameter synthesis problem is decidable for LTL properties. The investigated bounded integer parameter synthesis problem could be solved using an explicit enumeration of all possible parameter valuations. We propose an alternative symbolic zone-based method for this problem which results in a faster computation. Our technique extends the ideas of the automata-based approach to LTL m…
The reachability problem for timed automata asks if there exists a path from an initial state to a target state. The standard solution to this problem involves computing the zone graph of the automaton, which in principle could be infinite. In order to make the graph finite, zones are approximated using an extrapolation operator. For reasons of efficiency in current algorithms extrapolation of a zone is always a zone and in particular it is convex. In this paper, we propose to solve the reachability problem without such extrapolation operators. To ensure termination, we provide an efficient al…
The verification of systems combining hard timing constraints with concurrency is challenging. This challenge becomes even harder when some timing constants are missing or unknown. Parametric timed formalisms, such as parametric timed automata (PTAs), tackle the synthesis of such timing constants (seen as parameters) for which a property holds. Such formalisms are highly expressive, but also undecidable, and few decidable subclasses were proposed. We propose here a syntactic restriction on PTAs consisting in removing guards (constraints on transitions) to keep only invariants (constraints on l…
The process algebra tock-CSP provides textual notations for modelling discrete-time behaviours, with the support of various tools for verification. Similarly, automatic verification of Timed Automata (TA) is supported by the real-time verification toolbox UPPAAL. TA and tock-CSP differ in both modelling and verification approaches. For instance, liveness requirements are difficult to specify with the constructs of tock-CSP, but they are easy to verify in UPPAAL. In this work, we translate tock-CSP into TA to take advantage of UPPAAL. We have developed a translation technique and tool; our work…
We study the reachability problem for networks of timed communicating processes. Each process is a timed automaton communicating with other processes by exchanging messages over unbounded FIFO channels. Messages carry clocks which are checked at the time of transmission and reception with suitable timing constraints. Each automaton can only access its set of local clocks and message clocks of sent/received messages. Time is dense and all clocks evolve at the same rate. Our main contribution is a complete characterisation of decidable and undecidable communication topologies generalising and un…
