## List of Accepted Papers at FORMATS'08

 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 verificationof time Petri nets with stopwatches controlled by inhibitor arcs. We firstintroduce an extension of time Petri nets with inhibitor arcs (ITPNs) withtemporal parameters.  Then, we define a symbolic representation of theparametric state space based on the classical state class graph method. Theparameters of the model are embedded into the firing domains of the classes,that are represented by convex polyhedra. Finally, we propose semi-algorithmsfor the parametric model-checking of a subset of parametric TCTL formulae onITPNs.  We can thus generate the set of the parameter valuations that satisfythe 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 ofinherent 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 itsstate space abstractions: the state class graph (SCG) and the zonebased graph (ZBG). We show that only some time points of theclock/firing domains of abstract states are relevant to constructa TPN reachability graph. Moreover, for the state class graphmethod, the graph computed using relevant time points is smallerthan 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 thestructural aspects associated with task dependencies, with the dynamicaspects associated with ongoing streams of requests that arrive duringexecution. For this class of problems we develop a scheduling policywhich can guarantee bounded accumulation of backlog for all admissible request streams. We show, nevertheless,that no such policy can guarantee bounded latency for all requestpatterns. 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 thelanguage inclusion problem $L(A) \subseteq L(B)$ for a timed automaton$A$ and an  IRTA $B$ is decidable with doubly exponential timecomplexity.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 pricedtimed automata, are introduced.  Reachability-price and ratio-price problems for the  concavely priced timed are consideredand they are proved to be PSPACE-complete.  This paper generalises therecent work of Bouyer et al. on reachability-price and ratio-priceproblems 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 interpretedover (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 ofinfinite schedules for finite weighted automata and one-clock weightedtimed automata, subject to boundary constraints on the accumulatedweight.More specifically, we consider automata equipped with positive andnegative weights on transitions and locations, corresponding to theproduction and consumption of some resource (e.g. energy). We ask thequestion whether there exists an infinite path for which theaccumulated weight for any finite prefix satisfies certainconstraints: for the lower-bound problem, we require the accumulatedweight never drop below zero, for the interval-bound problem it is tostay within a given interval, and in the lower-weak-upper-boundproblem the accumulated weights may not drop below zero with theadditional feature that the weights never accumulate to more than agiven upper bound; any increases above this bound are simplytruncated. We also consider a game version of the above, where certaintransitions may be uncontrollable.For finite weighted automata we show that the lower- andlower-weak-upper-bound problems are decidable in polynomial time. Thisremains true even in the game setting, where we also prove P-hardnessof the problem.  The interval-bound problem is on the other handNP-hard but decidable in PSPACE (at least), and in the game setting itis EXPTIME-complete.For one-clock weighted timed automata, the lower- andlower-weak-upper-bound problems remain in P (also for the games), but theinterval-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 challengingindustrial case study that involves an existing state-of-the-art image processing pipeline.  Each ofthe resulting models is used to derive schedules for 7 concurrentjobs ("use cases") in the presence of limited resources (processingunits, 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 countingmodalities (TLC) is the extension  of  until-since temporal logicby counting modalities" C_n(X) and(n\in \nat); for each $n$ the modalityC_n(X) says that X will be true at least at n points in thenext unit of timeIn this paper we investigate the complexity of the satisfiabilityproblem for TLC and show that the problem is PSPACE complete whenthe index of C_n  is coded in unary, and EXPSPACE complete whenthe index is coded in binary. We also show that the satisfiabilityproblem for the until-since temporal logic extended by Pnueli'smodalities is PSPACE complete.