| Louis-Marie Traonouez, Didier Lime and Olivier H. Roux. Parametric model-checking of time Petri nets with stopwatches using the state-class graph |
| Abstract: In this paper, we propose a new framework for the parametric verification of time Petri nets with stopwatches controlled by inhibitor arcs. We first introduce an extension of time Petri nets with inhibitor arcs (ITPNs) with temporal parameters. Then, we define a symbolic representation of the parametric state space based on the classical state class graph method. The parameters of the model are embedded into the firing domains of the classes, that are represented by convex polyhedra. Finally, we propose semi-algorithms for the parametric model-checking of a subset of parametric TCTL formulae on ITPNs. We can thus generate the set of the parameter valuations that satisfy the formulae. |
| Jasper Berendsen and Frits Vaandrager. Compositional Abstraction in Real-Time Model Checking |
| Abstract: The idea to use simulations (or refinements) as a compositional abstraction device is well-known, both in untimed and timed settings, and has already been studied theoretically and practically in many papers during the last three decades. Nevertheless, existing approaches do not handle two fundamental modeling concepts which, for instance, are frequently used in the popular Uppaal model checker: (1) a parallel composition operator that supports communication via shared variables as well as synchronization of actions, and (2) committed locations. In this paper, we describe a framework for compositional abstraction based on simulation relations that does support both concepts, and that is suitable for Uppaal. Our approach is very general and the only essential restriction is that the guards of input transitions do not depend on external variables. We have applied our compositional framework to verify the Zeroconf protocol for an arbitrary number of hosts. |
| Mani Chandy, Concetta Pilotto and Sayan Mitra. Convergence Verification: From Synchronous to Partially Synchronous Systems |
| Abstract: Verification of partially synchronous distributed systems is difficult because of inherent concurrency and the potentially large state space of the channels. This paper identifies a subclass of such systems for which convergence properties can be verified based on the proof of convergence for the corresponding discrete-time shared state system. The proof technique extends to a class of partially synchronous systems in which an agent's state also evolves continuously over time. The proof techniques have been formalized in the PVS interface for timed I/O automata and applied to verify convergence of a mobile agent pattern formation algorithm. |
| Hanifa Boucheneb and Kamel Barkaoui. Relevant timed schedules / clock valuations for constructing time Petri net reachability graphs |
| Abstract: We consider here time Petri nets (the TPN model) and two of its state space abstractions: the state class graph (SCG) and the zone based graph (ZBG). We show that only some time points of the clock/firing domains of abstract states are relevant to construct a TPN reachability graph. Moreover, for the state class graph method, the graph computed using relevant time points is smaller than the SCG. |
| julien schmaltz and Jan Tretmans. On Conformance Testing for Timed Systems |
| Abstract: Conformance testing for labeled transition systems starts with defining when an implementation conforms to its specification. One of the formal theories for model-based testing uses the implementation relation $\ioco$ for this purpose. A peculiar aspect of $\ioco$ is to consider the absence of outputs as an observable action, named \emph{quiescence}. Recently a number of real-time extensions of ioco have been proposed in the literature. Quiescence and the observation of arbitrary delays are issues when defining such extensions. We present two new timed implementation relations and show their relation with existing ones. Based on these new definitions and using several examples, we show the subtle differences, and the consequences that small modifications in the definitions can have on the resulting relations. Moreover, we present conditions under which some of these implementation relations coincide. The notion of M-quiescence, i.e., if outputs occur in a system they occur before a delay M, turns out to be important in these conditions. |
| Michal Rutkowski, Marcin Jurdzinski, Ranko Lazic, Patricia Bouyer and Thomas Brihaye. Average-Price and Reachability-Price Games on Hybrid Automata with Strong Resets |
| Abstract: We introduce and study hybrid automata with strong resets. They generalize o-minimal hybrid automata, a class of hybrid automata which allows modeling of complex continuous dynamics. A number of analysis problems, such as reachability testing and controller synthesis, are decidable for classes of o-minimal hybrid automata. We generalize existing decidability results for controller synthesis on hybrid automata and we establish new ones by proving that average-price and reachability-price games on hybrid automata with strong resets are decidable, provided that the structure on which the hybrid automaton is defined has a decidable first-order theory. Our proof techniques include a novel characterization of values in games on hybrid automata by optimality equations, and a definition of a new finitary equivalence relation on the states of a hybrid automaton which enables a reduction of games on hybrid automata to games on finite graphs. |
| Aldric Degorre and Oded Maler. On Scheduling Policies for Streams of Structured Jobs |
| Abstract: We study a class of scheduling problems which combines the structural aspects associated with task dependencies, with the dynamic aspects associated with ongoing streams of requests that arrive during execution. For this class of problems we develop a scheduling policy which can guarantee bounded accumulation of backlog for all admissible request streams. We show, nevertheless, that no such policy can guarantee bounded latency for all request patterns. |
| Vijay Suman, Paritosh Pandya, Krishna S and Lakshmi Manasa G. Timed Automata with Integer Resets: Langauge Inclusion and Expressiveness |
| Abstract: In this paper, we consider a syntactic subset of timed automata called integer reset timed automata (IRTA) where {\em resets} are restricted to occur at integral time points. We argue with examples that the notion of global sparse time base used in time triggered architecture and distributed web services can naturally be modelled/specified as IRTA. As our main result, we show that the language inclusion problem $L(A) \subseteq L(B)$ for a timed automaton $A$ and an IRTA $B$ is decidable with doubly exponential time complexity. The expressive power and the closure properties of IRTA are also summarized. In particular, the IRTA are (highly succinct but) expressively equivalent to 1-clock deterministic IRTA and they are closed under boolean operations. |
| Marcin Jurdzinski and Ashutosh Trivedi. Concavely priced timed automata |
| Abstract: Concavely priced timed automata, a generalisation of linearly priced timed automata, are introduced. Reachability-price and ratio-price problems for the concavely priced timed are considered and they are proved to be PSPACE-complete. This paper generalises the recent work of Bouyer et al. on reachability-price and ratio-price problems for linearly priced timed automata. |
| Joost-Pieter Katoen and Alexandru Mereacre. Verifying Inhomogeneous Markov Chains |
| Abstract: This paper presents a stochastic variant of Hennessy-Milner logic that is interpreted over (state-labeled) inhomogeneous continuous-time Markov chains (ICTMCs), i.e., Markov chains in which transition rates are functions over time $t$. For piecewise constant rate functions, the model-checking problem is shown to be reducible to finding the zeros of an exponential polynomial. Using Sturm sequences and Newton's method, we obtain an approximative model-checking algorithm which is linear in the size of the ICTMC, logarithmic in the number of bits precision, and exponential in the nesting depth of the formula. |
| Carlo Alberto Furia and Matteo Rossi. MTL with Bounded Variability: Decidability and Complexity |
| Abstract: This paper investigates the properties of Metric Temporal Logic (MTL) over models in which time is dense but phenomena are constrained to have bounded variability. Contrary to the case of generic dense-time behaviors, MTL is proved to be fully decidable over models with bounded variability, if the variability bound is given. In these decidable cases, MTL complexity is shown to match that of simpler decidable logics such as MITL. On the contrary, MTL is undecidable if all behaviors with variability bounded by some generic constant are considered, but with an undecidability degree that is lower than in the case of generic behaviors. |
| Anne Remke and Boudewijn Haverkort. A uniformization-based algorithm for model checking CSL until operators on labelled queueing networks |
| Abstract: We present a model checking procedure for the CSL until operator on the CTMCs that underlie Jackson queueing networks. The key issue lies in the fact that the underlying CTMC is infinite in as many dimension as there are queues in the JQN. We need to compute the transient state probabilities for all goal states and for all possible starting states. However, for the transient probabilities no results are readily available. We use an unifromization-based apporach to compute the transient state probabilities. Furthermore, we show how the highly structured state space of JQNs then allows us to compute the possible infinite satisfaction set for until formulas. A case study on an e-business site shows the feasibility of our approach. |
| Krishnendu Chatterjee, Thomas Henzinger and Vinayak Prabhu. Timed Parity Games: Complexity and Robustness |
| Abstract: We consider concurrent two player games played in real time on timed automaton game structures with parity objectives. To disallow zeno-runs, we restrict both players to use only receptive strategies, which while ensuring that no player is responsible for blocking time, do not require any player to guarantee time-divergence. First, we present an efficient reduction of these games to turn-based finite state parity games. Hence the rich class of algorithms for turn-based parity games can now be applied to timed automaton parity games. As a consequence of our reduction we also improve the complexity of timed automaton parity games. Second, we consider two classes of robust strategies for the controller: namely, limit-robust and bounded-robust strategies. A limit-robust strategy of the controller must allow for some non-zero jitter in each of its moves.A bounded-robust strategy of the controller must allow for a jitter that is a known fixed constant for the system. We present efficient reduction to timed automaton games for solutions of both cases, and demonstrate that limit-robust strategies are strictly more powerful than bounded-robust strategies. |
| Patricia Bouyer, Uli Fahrenberg, Kim G. Larsen, Nicolas Markey and Jiri Srba. Infinite Runs in Weighted Timed Automata with Energy Constraints |
| 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: for the lower-bound problem, we require the accumulated weight never drop below zero, for the interval-bound problem it is to stay within a given interval, and in the lower-weak-upper-bound problem the accumulated weights may not drop below zero with the additional feature that the weights never accumulate to more than a given upper bound; any increases above this bound are simply truncated. We also consider a game version of the above, where certain transitions may be uncontrollable. For finite weighted automata we show that the lower- and lower-weak-upper-bound problems are decidable in polynomial time. This remains true even in the game setting, where we also prove P-hardness of the problem. The interval-bound problem is on the other hand NP-hard but decidable in PSPACE (at least), and in the game setting it is EXPTIME-complete. For one-clock weighted timed automata, the lower- and lower-weak-upper-bound problems remain in P (also for the games), but the interval-bound problem in the game setting is already undecidable. |
| Frits Vaandrager, Georgeta Igna, Venkatesh Kannan, Yang Yang, Twan Basten, Marc Geilen, Marc Voorhoeve, Sebastian De Smet and Lou Somers. Formal Modeling and Scheduling of Data Paths of Digital Document Printers |
| Abstract: We apply three different modeling frameworks --- timed automata (Uppaal), colored Petri nets and synchronous data flow --- to model a challenging industrial case study that involves an existing state-of-the-art image processing pipeline. Each of the resulting models is used to derive schedules for 7 concurrent jobs ("use cases") in the presence of limited resources (processing units, memory, USB bandwidth,..). The three models and corresponding analysis results are compared. |
| Frédéric Boniol, Hladik Pierre-Emmanuel and claire pagetti. A Framework for Distributing Real-Time Functions |
| Abstract: The design of critical embedded real-time systems requires high confidence in the architecture and the implemented functionalities. Classically, such functions are supported on a single monoprocessor, behavior of which is completely predictable, while the execution is totally deterministic. With the growing complexity of systems, it becomes quite unavoidable to implement these systems on distributed architectures. Scaling from mono to multiprocessor raises several issues which we address in this paper: we propose a simple executive model based on time triggered paradigm and an automated approach to allocate real-time tasks based on constraint resolution techniques. We illustrate the method on an industrial case study. |
| Alexander Rabinovich. Complexity of Metric Temporal logic with Counting |
| Abstract: The temporal logic with counting modalities (TLC) is the extension of until-since temporal logic by ``counting modalities" C_n(X) and (n\in \nat); for each $n$ the modality C_n(X) says that X will be true at least at n points in the next unit of time In this paper we investigate the complexity of the satisfiability problem for TLC and show that the problem is PSPACE complete when the index of C_n is coded in unary, and EXPSPACE complete when the index is coded in binary. We also show that the satisfiability problem for the until-since temporal logic extended by Pnueli's modalities is PSPACE complete. |