Some Bounds on the Computational Power of Piecewise Constant Derivative Systems

We study the computational power of Piecewise Constant Derivative (PCD) systems. PCD systems are dynamical systems defined by a piecewise constant differential equation and can be considered as computational machines working on a continuous space with a continuous time. We show that the computation time of these machines can be measured either as a discrete value, called discrete time, or as a continuous value, called continuous time. We relate the two notions of time for general PCD systems. We prove that general PCD systems are equivalent to Turing machines and linear machines in finite discrete time. We prove that the languages recognized by purely rational PCD systems in dimension d in finite continuous time are precisely the languages of the (d-2) th level of the arithmetical hierarchy. Hence the reachability problem of purely rational PCD systems of dimension d in finite continuous time is Σ _d-2 -complete. Received May 1997, and in final form May 1998.     

Verifying Programs with Unreliable Channels

We consider the verification of a particular class of infinite-state systems, namely systems consisting of finite-state processes that communicate via unbounded lossy FIFO channels. This class is able to model, e.g., link protocols such as the Alternating Bit Protocol and HDLC. For this class of systems, we show that several interesting verification problems are decidable by giving algorithms for verifying (1) thereachability problem—is a finite set of global states reachable from some other global state of the system ? (2)safety properties over tracesformulated as regular sets of allowed finite traces, and (3)eventuality properties—do all computations of a system eventually reach a given set of states? We have used the algorithms to verify some idealized sliding-window protocols with reasonable time and space resources. Our results should be contrasted with the well-known fact that these problems are undecidable for systems with unboundedperfectFIFO channels.     

Analysis of a class of communicating finite state machines

Thereachability, deadlok detection andunboundedness detection problems are considered for the class ofcyclic one-type message networks of communicating finite state machines. We show that all the three problems are effectively solvable by (a) constructing canonical execution event sequences which belong to a context-free language, and (b) showing that the reachability sets are semilinear. Our algorithms have polynomial complexity in terms of size of a global structure of a network, called theshuffle-product. The relationships between general Petri nets and the class of communicating finite state machines considered here are also explored.Supported in part by NSF CCR-9004121     

Symbolic backward reachability with effectively propositional logic

We describe a symbolic procedure for solving the reachability problem of transition systems that use formulae of Effectively Propositional Logic to represent sets of backward reachable states. We discuss the key ideas for the mechanization of the procedure where fix-point checks are reduced to SMT problems. We also show the termination of the procedure on a sub-class of transition systems. Then, we discuss how reachability problems for this sub-class can be used to encode analysis problems of administrative policies in the Role-Based Access Control (RBAC) model that is one of the most widely adopted access control paradigms. An implementation of a refinement of the backward reachability procedure, called asasp, shows better flexibility and scalability than a state-of-the-art tool on a significant set of security problems.     

O-Minimal Hybrid Systems

An important approach to decidability questions for verification algorithms of hybrid systems has been the construction of a bisimulation. Bisimulations are finite state quotients whose reachability properties are equivalent to those of the original infinite state hybrid system. In this paper we introduce the notion of o-minimal hybrid systems, which are initialized hybrid systems whose relevant sets and flows are definable in an o-minimal theory. We prove that o-minimal hybrid systems always admit finite bisimulations. We then present specific examples of hybrid systems with complex continuous dynamics for which finite bisimulations exist. Date received: June 9, 1998. Date revised: June 28, 1999.     

An approach to cyclic protocol validation

In this paper, the notion of fair reachability is generalized to cyclic protocols with more than two processes, where all the processes in a protocol are connected via a unidirectional ring and each process might contain internal transitions and can be non-deterministic. We identify ‘indefiniteness’ as a new type of logical error due to reachable internal transition cycles. By properly incorporating internal transitions into the formulation, we show that, with a few modifications, all the previous results established for cyclic protocols without non-deterministic and internal transitions still hold in the augmented model. Furthermore, by combining fair progress and maximal progress during state exploration, we prove that the following three problems are all decidable for Q, the class of cyclic protocols with finite fair reachable state spaces: (1) global state reachability; (2) abstract state reachability; and (3) execution cycle reachability. In the course of the investigation, we also show that detection of k-indefiniteness and k-livelock are decidable for Q.     

SAT-Solving the Coverability Problem for Petri Nets

Net unfoldings have attracted great attention as a powerful technique for combating state space explosion in model checking, and have been applied to verification of finite state systems including 1-safe (finite) Petri nets and synchronous products of finite transition systems. Given that net unfoldings represent the state space in a distributed, implicit manner the verification algorithm is necessarily a two step process: generation of the unfolding and reasoning about it. In his seminal work McMillan (K.L. McMillan, Symbolic Model Checking. Kluwer Academic Publishers, 1993) showed that deadlock detection on unfoldings of 1-safe Petri nets is NP-complete. Since the deadlock problem on Petri nets is PSPACE-hard it is generally accepted that the two step process will yield savings (in time and space) provided the unfoldings are small.In this paper we show how unfoldings can be extended to the context of infinite-state systems. More precisely, we show how unfoldings can be constructed to represent sets of backward reachable states of unbounded Petri nets in a symbolic fashion. Furthermore, based on unfoldings, we show how to solve the coverability problem for unbounded Petri nets using a SAT-solver. Our experiments show that the use of unfoldings, in spite of the two-step process for solving coverability, has better time and space characteristics compared to a traditional reachability based implementation that considers all interleavings for solving the coverability problem.     

Synchronizing sequences on a class of unbounded systems using synchronized Petri nets

Determining the state of a system when one does not know its current initial state is a very important problem in many practical applications as checking communication protocols, part orienteers, digital circuit reset, etc. Synchronizing sequences have been proposed in the 60’s to solve the problem on systems modeled by finite state machines. This paper presents a first investigation of the synchronizing problem on unbounded systems, using synchronized Petri nets, i.e., nets whose evolution is driven by external input events. The proposed approach suffers from the fact that no finite space representation can exhaustively answer to the reachability problem but we show that synchronizing sequences may be computed for a particular class of unbounded synchronized Petri nets.     

Verifying lossy channel systems has nonprimitive recursive complexity

Lossy channel systems are systems of finite state automata that communicate via unreliable unbounded fifo channels. It is known that reachability, termination and a few other verification problems are decidable for these systems. In this article we show that these problems cannot be solved in primitive recursive time.     

Reverse reachability analysis: A new technique for deadlock detection on communicating finite state machines

The communicating finite state machines can exchange messages over bounded FIFO channels. In this paper, a new technique, called reverse reachability analysis, is proposed to detect deadlocks on the communication between the communicating finite state machines. The technique is based on finding reverse reachable paths starting from possible deadlock states. If a reverse reachable path can reach the initial global state, then deadlock occurs. Otherwise the communication is deadlock-free. The effectiveness of the technique has been verified by some real protocols such as a specification of X.25 call establishment/clear protocol and Bartlet's alternating bit protocol.     

On Equilibria in Quantitative Games with Reachability/Safety Objectives

In this paper, we study turn-based multiplayer quantitative non zero-sum games played on finite graphs with reachability objectives. In this framework each player aims at reaching his own goal as soon as possible. We focus on existence results for two solution concepts: Nash equilibrium and secure equilibrium. We prove the existence of finite-memory Nash (resp. secure) equilibria in n-player (resp. 2-player) games. For the case of Nash equilibria, we extend our result in two directions. First, we show that finite-memory Nash equilibria still exist when the model is enriched by allowing n-tuples of positive costs on edges (one cost by player). Secondly, we prove the existence of Nash equilibria in quantitative games with both reachability and safety objectives.     

Termination Proofs for String Rewriting Systems via Inverse Match-Bounds

Annotating a letter by a number, one can record information about its history during a rewrite derivation. In each rewrite step, numbers in the reduct are updated depending on the redex numbering. A string rewriting system is called match-bounded if there is a global upper bound to these numbers. Match-boundedness is known to be a strong sufficient criterion for both termination and preservation of regular languages. We show that the string rewriting systems whose inverse (left and right hand sides exchanged) is match-bounded, also have exceptional properties, but slightly different ones. Inverse match-bounded systems need not terminate; they effectively preserve context-free languages; their sets of normalizable strings and their sets of immortal strings are effectively regular. These languages can be used to decide the normalization, the uniform normalization, the termination and the uniform termination problem for inverse match-bounded systems. We also prove that the termination problem is decidable in linear time, and that a certain strong reachability problem is decidable, thereby solving two open problems of McNaughton’s. Like match-bounds, inverse match-bounds entail linear derivational complexity on the set of terminating strings.     

A unified approach for studying the properties of transition systems

In this paper a systematic method for generating, comparing and proving the properties of transition systems is presented. It is assumed that any property of a system can be defined by giving a set of ‘target’ states and a type of reachability. Ten different types of reachability are proposed; by appropriately choosing the set of target states, a family of ten potentially different properties is generated. The main conclusion is that the reachability types and therefore the system properties, can be characterized by simple relations involving the set of the possible initial states and fixed points of certain continuous predicate trasformers depending on the set of target states. As a consequence, in order to prove a given property it is sufficient to compute iteratively greatest or least fixed points of continuous predicate transformers.Some examples are presented which show how the results can be applied to prove the properties of concurrent systems represented by non-deterministic models.     

Computing Accumulated Delays in Real-time Systems

We present a verification algorithm for duration properties of real-time systems. While simple real-time properties constrain the total elapsed time between events, duration properties constrain the accumulated satisfaction time of state predicates. We formalize the concept of durations by introducing duration measures for timed automata. A duration measure assigns to each finite run of a timed automaton a real number —the duration of the run— which may be the accumulated satisfaction time of a state predicate along the run. Given a timed automaton with a duration measure, an initial and a final state, and an arithmetic constraint, the duration-bounded reachability problem asks if there is a run of the automaton from the initial state to the final state such that the duration of the run satisfies the constraint. Our main result is an (optimal) PSPACE decision procedure for the duration-bounded reachability problem.     

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.     

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 for Hybrid Logic

We consider the model checking problem for Hybrid Logic. Known algorithms so far are global in the sense that they compute, inductively, in every step the set of all worlds of a Kripke structure that satisfy a subformula of the input. Hence, they always exploit the entire structure. Local model checking tries to avoid this by only traversing necessary parts of the input in order to establish or refute the satisfaction relation between a given world and a formula. We present a framework for local model checking of Hybrid Logic based on games. We show that these games are simple reachability games for ordinary Hybrid Logic and weak Büchi games for Hybrid Logic with operators interpreted over the transitive closure of the accessibility relation of the underlying Kripke frame, and show how to solve these games thus solving the local model checking problem. Since the first-order part of Hybrid Logic is inherently hard to localise in model checking, we give examples, in the end, of how global model checkers can be optimised in certain special cases using well-established techniques like fixpoint approximations and divide-and-conquer algorithms.     

An Automata-Theoretic Approach to the Reachability Analysis of RPPS Systems

We show how the tree-automata techniques proposed by Lugiez and Schnoebelen apply to the reachability analysis of RPPS systems. Using these techniques requires that we express the states of RPPS systems in a tailor-made process rewrite system where reachability is a relation recognizable by finite tree-automata.     

Verification of Similar FSMs by Mixing Incremental Re-encoding, Reachability Analysis, and Combinational Checks

State space exploration is often used to prove properties about sequential behavior of Finite State Machines (FSMs). For example, equivalence of two machines is proved by analyzing the reachable state set of their product machine. Nevertheless, reachability analysis is infeasible on large practical examples. Combinational verification is far less expensive, but on the other hand its application is limited to combinational circuits, or particular design schemes. Finally, approximate techniques imply sufficient, not strictly necessary conditions.The purpose of this paper is to extend the applicability of purely combinational checks. This is generally achieved through state minimization, partitioning, and re-encoding the FSMs to factor out their differences. We focus on re-encoding. In particular, we present an incremental approach to re-encoding for verification that transforms the product machine traversal into a combinational verification in the best case, and into a computationally simpler product machine traversal in the general case.Experimental results demonstrate the effectiveness of this technique on medium-large circuits where other techniques may fail.     

Regular Model Checking Using Inference of Regular Languages

Regular model checking is a method for verifying infinite-state systems based on coding their configurations as words over a finite alphabet, sets of configurations as finite automata, and transitions as finite transducers. We introduce a new general approach to regular model checking based on inference of regular languages. The method builds upon the observation that for infinite-state systems whose behaviour can be modelled using length-preserving transducers, there is a finite computation for obtaining all reachable configurations up to a certain length n. These configurations are a (positive) sample of the reachable configurations of the given system, whereas all other words up to length n are a negative sample. Then, methods of inference of regular languages can be used to generalize the sample to the full reachability set (or an overapproximation of it). We have implemented our method in a prototype tool which shows that our approach is competitive on a number of concrete examples. Furthermore, in contrast to all other existing regular model checking methods, termination is guaranteed in general for all systems with regular sets of reachable configurations. The method can be applied in a similar way to dealing with reachability relations instead of reachability sets too.