Inclusion dynamics hybrid automata

Hybrid systems are dynamical systems with the ability to describe mixed discrete-continuous evolution of a wide range of systems. Consequently, at first glance, hybrid systems appear powerful but recalcitrant, neither yielding to analysis and reasoning through a purely continuous-time modeling as with systems of differential equations, nor open to inferential processes commonly used for discrete state-transition systems such as finite state automata. A convenient and popular model, called hybrid automata, was introduced to model them and has spurred much interest on its tractability as a tool for inference and model checking in a general setting. Intuitively, a hybrid automaton is simply a “finite-state” automaton with each state augmented by continuous variables, which evolve according to a set of well-defined continuous laws, each specified separately for each state. This article investigates both the notion of hybrid automaton and the model checking problem over such a structure. In particular, it relates first-order theories and analysis results on multivalued maps and reduces the bounded reachability problem for hybrid automata whose continuous laws are expressed by inclusions (x′f(x,t)) to a decidability problem for first-order formulæ over the reals. Furthermore, the paper introduces a class of hybrid automata for which the reachability problem can be decided and shows that the problem of deciding whether a hybrid automaton belongs to this class can be again decided using first-order formulæ over the reals. Despite the fact that the bisimulation quotient for this class of hybrid automata can be infinite, we show that our techniques permit effective model checking for a nontrivial fragment of CTL.     

Model Checking Weighted Integer Reset Timed Automata

Weighted timed automata (WTA), introduced in Alur et al. (Proceedings of HSCC’01, LNCS, vol. 2034, pp. 49–62, Springer, Berlin, 2001), Behrmann et al. (Proceedings of HSCC’01, LNCS, vol. 2034, pp. 147–161, Springer, Berlin, 2001) are an extension of Alur and Dill (Theor. Comput. Sci. 126(2):183–235, 1994) timed automata, a widely accepted formalism for the modelling and verification of real time systems. Weighted timed automata extend timed automata by allowing costs on the locations and edges. There has been a lot of interest Bouyer et al. (Inf. Process. Lett. 98(5):188–194, 2006), Bouyer et al. (Log. Methods Comput. Sci. 4(2):9, 2008), Brihaye et al. (Proceedings of FORMATS/FTRTFT’04, LNCS, vol. 3253, pp. 277–292, Springer, Berlin, 2004), Brihaye et al. (Inf. Comput. 204(3):408–433, 2006) in studying the model checking problem of weighted timed automata. The properties of interest are written using logic weighted CTL (WCTL), an extension of CTL with costs. It has been shown Bouyer et al. (Log. Methods Comput. Sci. 4(2):9, 2008) that the problem of model checking WTAs with a single clock using WCTL with no external cost variables is decidable, while 3 clocks render the problem undecidable Bouyer et al. (Inf. Process. Lett. 98(5):188–194, 2006). The question of 2 clocks is open. In this paper, we introduce a subclass of weighted timed automata called weighted integer reset timed automata (WIRTA) and study the model checking problem. We give a clock reduction technique for WIRTA. Given a WIRTA A\mathcal{A} with n≥1 clocks, we show that a single clock WIRTA A￠\mathcal{A}' preserving the paths and costs of A\mathcal{A} can be obtained. This gives us the decidability of model checking WIRTA with n≥1 clocks and m≥1 costs using WCTL with no external cost variables. We then show that for a restricted version of WCTL with external cost variables, the model checking problem is undecidable for WIRTA with 3 stopwatch costs and 1 clock. Finally, we show that model checking WTA with 2 clocks and 1 stopwatch cost against WCTL with no external cost variables is undecidable, thereby answering a question that has remained long open.     

Liveness Checking as Safety Checking for Infinite State Spaces

In previous work we have developed a syntactic reduction of repeated reachability to reachability for finite state systems. This may lead to simpler and more uniform proofs for model checking of liveness properties, help to find shortest counterexamples, and overcome limitations of closed-source model-checking tools. In this paper we show that a similar reduction can be applied to a number of infinite state systems, namely, (ω−)regular model checking, push-down systems, and timed automata.     

Language-Emptiness Checking of Alternating Tree Automata Using Symbolic Reachability Analysis

Alternating tree automata and AND/OR graphs provide elegant formalisms that enable branching- time logics to be verified in linear time. The seminal work of Kupferman et al. [Orna Kupferman, Moshe Y. Vardi, and Pierre Wolper. An automata-theoretic approach to branching-time model checking. J. ACM, 47(2):312–360, 2000] showed that 1) branching-time model checking is reducible to the language non-emptiness checking of the product of two alternating automata representing the model and property under verification, and 2) the non-emptiness problem can be solved by performing a search on an AND/OR graph representing this product. Their algorithm, however, can only be implemented in an explicit-state model checker because it needs stacks to detect accept and reject runs. In this paper, we propose a BDD-based approach to check the language non-emptiness of the product automaton. We use a technique called “state recording” from Schuppan and Biere [Viktor Schuppan and Armin Biere. Efficient reduction of finite state model checking to reachability analysis. Int. Journal on Software Tools for Technology Transfer (STTT), 5(2–3):185–204, 2004] to emulate the stack mechanism from explicit-state model checking. This technique allows us to transform the product automaton into a well-defined AND/OR graph. We develop a BDD-based reachability algorithm to efficiently determine whether a solution graph for the AND/OR graph exists and thereby solve the model-checking problem. While “state recording” increases the size of the state space, the advantage of our approach lies in the memory saving BDDs can offer and the potential it opens up for optimisation of the reachability analysis. We remark that this technique always detects the shortest counter-example.     

Predicate Abstraction for Dense Real-Time Systems

We propose predicate abstraction as a means for verifying a rich class of safety and liveness properties for dense real-time systems. First, we define a restricted semantics of timed systems which is observationally equivalent to the standard semantics in that it validates the same set of μ-calculus formulas without a next-step operator. Then, we recast the model checking problem S for a timed automaton S and a μ-calculus formula in terms of predicate abstraction. Whenever a set of abstraction predicates forms a so-called basis, the resulting abstraction is strongly preserving in the sense that S validates iff the corresponding finite abstraction validates this formula . Now, the abstracted system can be checked using familiar μ-calculus model checking. Like the region graph construction for timed automata, the predicate abstraction algorithm for timed automata usually is prohibitively expensive. In many cases it suffices to compute an approximation of a finite bisimulation by using only a subset of the basis of abstraction predicates. Starting with some coarse abstraction, we define a finite sequence of refined abstractions that converges to a strongly preserving abstraction. In each step, new abstraction predicates are selected nondeterministically from a finite basis. Counterexamples from failed μ-calculus model checking attempts can be used to heuristically choose a small set of new abstraction predicates for refining the abstraction.     

Interval Duration Logic: Expressiveness and Decidability

We investigate a variant of dense-time Duration Calculus which permits model checking using timed/hybrid automata. We define a variant of the Duration Calculus, called Interval Duration Logic, (IDL), whose models are timed state sequences [1].A subset LIDL of IDL consisting only of located time constraints is presented. As our main result, we show that the models of an LIDL formula can be captured as timed state sequences accepted by an event-recording integrator automaton. A tool called IDLVALID for reducing LIDL formulae to integrator automata is briefly described. Finally, it is shown that LIDL has precisely the expressive power of event-recording integrator automata, and that a further subset LIDL- corresponds exactly to event-recording timed automata [2]. This gives us an automata-theoretic decision procedure for the satisfiability of LIDL– formulae.     

Network invariants for real-time systems

We extend the approach of model checking parameterized networks of processes by means of network invariants to the setting of real-time systems. We introduce timed transition structures (which are similar in spirit to timed automata) and define a notion of abstraction that is safe with respect to linear temporal properties. We strengthen the notion of abstraction to allow a finite system, then called network invariant, to be an abstraction of networks of real-time systems. In general the problem of checking abstraction of real-time systems is undecidable. Hence, we provide sufficient criteria, which can be checked automatically, to conclude that one system is an abstraction of a concrete one. Our method is based on timed superposition and discretization of timed systems. We exemplify our approach by proving mutual exclusion of a simple protocol inspired by Fischer’s protocol, using the model checker TLV. Part of this work was done during O. Grinchtein’s stay at Weizmann Institute. This author was supported by the European Research Training Network “Games”.     

有关时间自动机重置的若干问题的计算复杂性

自动机的重置序列也称为同步序列,具有以下特性：有限自动机通过运行重置序列w,可从任意一个未知的或无法观测到的状态q₀到达某个特定状态q_w.这仅依赖于w,而与开始运行w时的状态q₀无关.这一特性可用于部分可观察的复杂系统的自动恢复,而无需重启,甚至有时不能重启.基于此,重置问题自出现以来便得到关注和持续研究.最近几年,它被扩展到可以描述诸如分布式、嵌入式实时系统等复杂系统的无限状态模型上,比如时间自动机和寄存器自动机等.以时间自动机的重置问题的计算复杂性为研究对象,发现重置问题与可达性问题有着紧密的联系.主要贡献是：（1）利用时间自动机可达性问题的最新成果,完善完全的确定的时间自动机重置问题的计算复杂性结论;（2）对部分规约的确定的时间自动机,研究得出,即使在输入字母表大小减至2的情况下,其复杂性仍是PSPACE-完全的;特别地,在单时钟情况下是NLOGSPACE-完全的;（3）对完全的非确定的时间自动机,研究得出其D_i-可重置问题（i=1,2,3）是不可判定的,其重置问题与非确定的寄存器自动机重置问题在指数时间可以相互归约,通过证明指数时间归约相对高复杂性类具有封闭性,利用非确定的寄存器自动机的结论得出单时钟的时间自动机的重置问题是Ackermann-完全的、限界的重置问题是NEXPTIME-完全的.这些复杂性结论,说明关于时间自动机的重置问题大都是难解的,一方面,为时间系统的可重置性的检测和求解奠定坚实的理论基础,另一方面,为以后寻找具有高效算法的特殊结构的时间系统（即具有高效算法的问题子类）给予理论指导.     

Timed Modal Logics for Real-Time Systems

In this paper, a timed modal logic L _c is presented for the specification and verification of real-time systems. Several important results for L _c are discussed. First we address the model checking problem and we show that it is an EXPTIME-complete problem. Secondly we consider expressiveness and we explain how to express strong timed bisimilarity and how to build characteristic formulas for timed automata. We also propose a compositional algorithm for L _c model checking. Finally we consider several control problems for which L _c can be used to check controllability.     

Termination Criteria for Bounded Model Checking: Extensions and Comparison

Increasing attention has been paid recently to criteria that allow one to conclude that a structure models a linear-time property from the knowledge that no counterexamples exist up to a certain length. These termination criteria effectively turn Bounded Model Checking into a full-fledged verification technique and sometimes result in considerable time savings. In [M. Awedh and F. Somenzi. Proving more properties with bounded model checking. In R. Alur and D. Peled, editors, Sixteenth Conference on Computer Aided Verification (CAV'04), pages 96–108. Springer-Verlag, Berlin, July 2004. LNCS 3114] we presented a criterion based on the translation of the linear-time specification into a Büchi automaton. BMC can be terminated if no fair cycle is found up to a given length, and one can prove that no fair cycle exists beyond that length. The maximum length for which counterexamples are explicitly checked is called the termination length; it obviously depends on the model, the property, and the termination criterion. In this paper we improve the criterion of [M. Awedh and F. Somenzi. Proving more properties with bounded model checking. In R. Alur and D. Peled, editors, Sixteenth Conference on Computer Aided Verification (CAV'04), pages 96–108. Springer-Verlag, Berlin, July 2004. LNCS 3114] by adding a check that often substantially reduces termination length. Our previous work employed translation to a non-generalized Büchi automaton. Though a well-known technique converts a generalized automaton into that form by composing it with a counter, it has the undesirable effect of considerably lengthening the cycles in the graph to be searched. We propose several alternatives to that approach and compare them experimentally. The translation to automata can be accomplished in more than one way, and in this paper we contrast two of them: one based on the algorithms of [F. Somenzi and R. Bloem. Efficient Büchi automata from LTL formulae. In E. A. Emerson and A. P. Sistla, editors, Twelfth Conference on Computer Aided Verification (CAV'00), pages 248–263. Springer-Verlag, Berlin, July 2000. LNCS 1855], and one based on the notion of tight automaton of [E. Clarke, O. Grumberg, and K. Hamaguchi. Another look at LTL model checking. In D. L. Dill, editor, Sixth Conference on Computer Aided Verification (CAV'94), pages 415–427. Springer-Verlag, Berlin, 1994. LNCS 818]. The latter yields shorter counterexamples, but the former often leads to earlier termination. In addition, it can help in identifying safety properties, for which termination checks are much more efficient than for the general case. We finally present results on comparing techniques based on cycle detection to the technique of [V. Schuppan and A. Biere. Efficient reduction of finite state model checking to reachability analysis. Software Tools for Technology Transfer, 5(2–3):185–204, Mar. 2004], which converts liveness properties into safety properties by augmentation of the model.     

Communication Complexity Method for Measuring Nondeterminism in Finite Automata

While deterministic finite automata seem to be well understood, surprisingly many important problems concerning nondeterministic finite automata (nfa's) remain open. One such problem area is the study of different measures of nondeterminism in finite automata and the estimation of the sizes of minimal nondeterministic finite automata. In this paper the concept of communication complexity is applied in order to achieve progress in this problem area. The main results are as follows:1. Deterministic communication complexity provides lower bounds on the size of nfa's with bounded unambiguity. Applying this fact, the proofs of several results about nfa's with limited ambiguity can be simplified and presented in a uniform way.2. There is a family of languages KON_k² with an exponential size gap between nfa's with polynomial leaf number/ambiguity and nfa's with ambiguity k. This partially provides an answer to the open problem posed by B. Ravikumar and O. Ibarra (1989, SIAM J. Comput.18, 1263–1282) and H. Leung (1998, SIAM J. Comput.27, 1073–1082).     

基于SMT的PTACTL限界模型检测方法

概率时间自动机是在时间自动机的基础上加上各个状态迁移的概率以后形成的一种扩展的时间自动机,能用来对基于时间的随机协议、容错系统等进行建模,具有很强的实用性。本文针对概率时间自动机给出一种基于SMT的限界模型检测方法来验证该模型下的PTACTL性质,该方法由基于SMT的限界模型检测算法演变而来,通过将迁移时间和迁移概率融入ACTL性质中,改变模型的编码以及待验证性质的编码方式来实现对性质的验证。通过2个实例说明检测过程的有效性和高效性。     

Event clock message passing automata: a logical characterization and an emptiness checking algorithm

We are interested in modeling behaviors and verifying properties of systems in which time and concurrency play a crucial role. We introduce a model of distributed automata which are equipped with event clocks as in Alur et al. (Theor Comput Sci 211:253–273, 1999), which we call Event Clock Message Passing Automata (ECMPA). To describe the behaviors of such systems we use timed partial orders (modeled as message sequence charts with timing). Our first goal is to extend the classical Büchi-Elgot-Trakhtenbrot equivalence to the timed and distributed setting, by showing an equivalence between ECMPA and a timed extension of monadic second-order (MSO) logic. We obtain such a constructive equivalence in two different ways: (1) by restricting the semantics by bounding the set of timed partial orders; (2) by restricting the timed MSO logic to its existential fragment. We next consider the emptiness problem for ECMPA, which asks if a given ECMPA has some valid timed execution. In general this problem is undecidable and we show that by considering only bounded timed executions, we can obtain decidability. We do this by constructing a timed automaton which accepts all bounded timed executions of the ECMPA and checking emptiness of this timed automaton.     

An estimate on the convergence of MKZ–Bézier operators

The pointwise approximation properties of the MKZ–Bézier operators M_n,α(f,x) for α≥1 have been studied in [X.M. Zeng, Rates of approximation of bounded variation functions by two generalized Meyer–König–Zeller type operators, Comput. Math. Appl. 39 (2000) 1–13]. The aim of this paper is to study the pointwise approximation of the operators M_n,α(f,x) for the other case 0<α<1. By means of some new estimate techniques and a result of Guo and Qi [S. Guo, Q. Qi, The moments for the Meyer–König and Zeller operators, Appl. Math. Lett. 20 (2007) 719–722], we establish an estimate formula on the rate of convergence of the operators M_n,α(f,x) for the case 0<α<1.     

Closed, Open, and Robust Timed Networks

We consider verification of safety properties for parameterized systems of timed processes, so called timed networks. A timed network consists of a finite state process, called a controller, and an arbitrary set of identical timed processes. In [Parosh Aziz Abdulla and Bengt Jonsson. Model checking of systems with many identical timed processes. Theoretical Computer Science, 290(1):241–264, 2003] it was shown that checking safety properties is decidable in the case where each timed process is equipped with a single real-valued clock. In [P. Abdulla, J. Deneux, and P. Mahata. Multi-clock timed networks. In Proc. LICS' 04, pages 345–354. IEEE Computer Society Press, 2004], we showed that this is no longer possible if each timed process is equipped with at least two real-valued clocks. In this paper, we study two subclasses of timed networks: closed and open timed networks. In closed timed networks, all clock constraints are non-strict, while in open timed networks, all clock constraints are strict (thus corresponds to syntactic removal of equality testing). We show that the problem becomes decidable for closed timed network, while it remains undecidable for open timed networks. We also consider robust semantics of timed networks by introducing timing fuzziness through semantic removal of equality testing. We show that the problem is undecidable both for closed and open timed networks under the robust semantics.     

Non uniform random generation of generalized Motzkin paths

We consider in this paper the class M _k ⁿ of generalized Motzkin paths of length n, that is, lattice paths using steps (1,1), (1,−1), (k,0), where k is a fixed positive integer, starting at the origin (0,0), running above the x-axis, and ending at (n,0). The area is the region bounded by the path and the x-axis. We first establish a bijection between the area of paths in M _k ⁿ and some lattice paths of length n+1. Then, by using a rejection technique, we obtain a linear algorithm with an average time complexity (k mod 2 +1)(n+1).With the support of NSERC (Canada), G.N.C.S. – Istituto Nazionale di Alta Matematica (Italia), MIUR Project: Linguaggi Formalie Automi: Teoriae Applicazioni     

A Cost-Optimal Pipeline Algorithm for Permutation Generation in Lexicographic Order

In this paper we solve the open problem of designing a cost-optimal parallel algorithm for generating permutations ofMelements out of the set {0, 1, …,N− 1}, in lexicographic order. Our algorithm runs on the simplest model of parallel computation, i.e., a linear array of sizeM, where each processor PE(i) needs only a constant number of words of length logN, and is responsible for producing with constant delay, theith components in the successive permutations. This algorithm runs in timeO(N!/(N−M)!) on an array of sizeMand is therefore cost-optimal when the time needed to output the permutations is taken into account. Moreover, by doubling the number of cells, it is possible to implement this algorithm on a unidirectional linear array.     

Connectivity properties of spaces of partial realizations

This paper addresses the problem of determining the number of connected components of the space of real scalar M×N Hankel matrices of rank n. For n<min{M,N} it is shown that the space has n+1 components for M+N even, and is connected for M+N odd. As an application, the number of components of sets of minimal partial realizations of McMillan degree nτ of length τ sequences is determined.     

Task automata: Schedulability,decidability and undecidability

We present a model, task automata, for real time systems with non-uniformly recurring computation tasks. It is an extended version of timed automata with asynchronous processes that are computation tasks generated (or triggered) by timed events. Compared with classical task models for real time systems, task automata may be used to describe tasks (1) that are generated non-deterministically according to timing constraints in timed automata, (2) that may have interval execution times representing the best case and the worst case execution times, and (3) whose completion times may influence the releases of task instances. We generalize the classical notion of schedulability to task automata. A task automaton is schedulable if there exists a scheduling strategy such that all possible sequences of events generated by the automaton are schedulable in the sense that all associated tasks can be computed within their deadlines. Our first technical result is that the schedulability for a given scheduling strategy can be checked algorithmically for the class of task automata when the best case and the worst case execution times of tasks are equal. The proof is based on a decidable class of suspension automata: timed automata with bounded subtraction in which clocks may be updated by subtractions within a bounded zone. We shall also study the borderline between decidable and undecidable cases. Our second technical result shows that the schedulability checking problem will be undecidable if the following three conditions hold: (1) the execution times of tasks are intervals, (2) the precise finishing time of a task instance may influence new task releases, and (3) a task is allowed to preempt another running task.     

Decision problems for lower/upper bound parametric timed automata

We investigate a class of parametric timed automata, called lower bound/upper bound (L/U) automata, where each parameter occurs in the timing constraints either as a lower bound or as an upper bound. For such automata, we show that basic decision problems, such as emptiness, finiteness and universality of the set of parameter valuations for which there is a corresponding infinite accepting run of the automaton, is Pspace-complete. We extend these results by allowing the specification of constraints on parameters as a linear system. We show that the considered decision problems are still Pspace-complete, if the lower bound parameters are not compared with the upper bound parameters in the linear system, and are undecidable in general. Finally, we consider a parametric extension of MITL\mathsf{MITL} _0,∞, and prove that the related satisfiability and model checking (w.r.t. L/U automata) problems are Pspace-complete.