Oded Maler: Abstracts of Conference Papers

  • O. Maler, A. Pnueli, Tight Bounds on the Complexity of Cascaded Decomposition of Automata. In this paper we give exponential upper and lower bounds on the size of the cascaded (Krohn-Rhodes) decomposition of automata. These results are used for giving elementary algorithms for various translations between automata and temporal logic, where the previously-known translations were non-elementary.

  • O. Maler, Z. Manna A. Pnueli, From Timed to Hybrid Systems.[Pdf]

  • E. Asarin, O. Maler, On some Relations between Dynamical Systems and Transition Systems. In this paper we define a precise notion of abstraction relation between continuous dynamical systems and discrete state-transition systems. Our main result states that every Turing Machine can be realized by a dynamical system with piecewise-constant derivatives in a 3-dimensional space and thus the reachability problem for such systems is undecidable for 3 dimensions. A decision procedure for 2-dimensional systems has been recently reported by Maler and Pnueli. On the other hand we show that some non-deterministic finite automata cannot be realized by any continuous dynamical system with less than 3 dimensions. [Pdf]

  • O. Maler, A.Pnueli, J.Sifakis, On the Synthesis of Discrete Controllers for Timed Systems. This paper presents algorithms for the automatic synthesis of real-time controllers by finding a winning strategy for certain games defined by the timed-automata of Alur and Dill. In such games, the outcome depends on the players' actions as well as on their timing. We believe that these results will pave the way for the application of program synthesis techniques to the construction of real-time embedded systems from their specifications. [Pdf]

  • E.Asarin, O. Maler and A.Pnueli, Symbolic Controller Synthesis for Discrete and Timed Systems. This paper presents algorithms for the symbolic synthesis of discrete and real-time controllers. At the semantic level the controller is synthesized by finding a winning strategy for certain games defined by automata or by timed-automata. The algorithms for finding such strategies need, this way or another, to search the state-space of the system which grows exponentially with the number of components. Symbolic methods allow such a search to be conducted without necessarily enumerating the state-space. This is achieved by representing sets of states using formulae (syntactic objects) over state variables. Although in the worst case such methods are as bad as enumerative ones, many huge practical problems can be treated by fine-tuned symbolic methods. In this paper the scope of these methods is extended from analysis to synthesis and from purely discrete systems to real-time systems.

    • We believe that these results will pave the way for the application of program synthesis techniques to the construction of real-time embedded systems from their specifications and to a solution of other related design problems associated with real-time systems in general and asynchronous circuits in particular. [Pdf]

  • O. Maler, A. Pnueli, Timing Analysis of Asynchronous Circuits using Timed Automata. In this paper we present a method for modeling asynchronous digital circuits by timed automata. The constructed timed automata serve as "mechanical" and verifiable objects for asynchronous sequential machines in the same sense that (untimed) automata do for synchronous machines. These results, combined with recent results concerning the analysis and synthesis of timed automata provide for the systematic treatment of a large class of problems that could be treated by conventional simulation methods only in an ad-hoc fashion. The problems that can be solved due to the results presented in this paper include: the reachability analysis of a circuit with uncertainties in gate delays and input arrival times, inferring the necessary timing constraints on input signals that guarantee a proper functioning of a circuit and calculating the delay characteristics of the components required in order to meet some given behavioral specifications.

    • Notwithstanding the existence of negative theoretical results concerning the worst-case complexity of timed automata analysis algorithms, initial experimentation with the Kronos tool for timing analysis suggest that timed automata derived from circuits might not be so hard to analyze in practice. [Pdf]

  • O. Maler, S. Yovine, Hardware Timing Verification using KRONOS. In this paper we describe the KRONOS system, a tool for verifying real-time properties based on the model of timed-automata. As an example, we show how KRONOS is applied to the verification of a MOS circuit under various delay assumptions. [Pdf]

  • E. Asarin, M. Bozga, A. Kerbrat, O. Maler, A. Pnueli, A. Rasse, Data-Structures for the Verification of Timed Automata. In this paper we suggest numerical decision diagrams , a BDD-based data-structure for representing certain subsets of the Euclidean space, namely those encountered in verification of timed automata. Unlike other representation schemes, NDD's are canonical and provide for all the necessary operations needed in the verification and synthesis of timed automata. We report some preliminary experimental results. [Pdf]

  • E. Asarin, O. Maler, P. Caspi, A Kleene Theorem for Timed Automata. In this paper we define timed regular expressions, an extension of regular expressions for specifying sets of dense-time discrete-valued signals. We show that this formalism is equivalent in expressive power to the timed automata of Alur and Dill by providing a translation procedure from expressions to automata and vice versa. The result is extended to omega-regular expressions (Buchi's theorem). [Pdf]

  • M. Bozga, O. Maler, A. Pnueli, S. Yovine, Some Progress in the Symbolic Verification of Timed Automata. In this paper we discuss the practical difficulty of analyzing the behavior of timed automata and report some results obtained using an experimental BDD-based extension of KRONOS. We have treated examples originating from timing analysis of asynchronous boolean networks and CMOS circuits with delay uncertainties and the results outperform those obtained by previous implementations of timed automata verification tools. [Pdf]

  • A. Bouajjani, J. Esparza, O. Maler, Reachability Analysis of Pushdown Automata: Application to Model-Checking. We apply the symbolic analysis principle to pushdown systems. We represent (possibly infinite) sets of configurations of such systems by means of finite-state automata. In order to reason in a uniform way about analysis problems involving both existential and universal path quantification (such as model-checking for branching-time logics), we consider the more general class of alternating pushdown systems and use alternating finite-state automata as a representation structure for sets of their configurations. We give a simple and natural procedure to compute sets of predecessors using this representation structure. We incorporate this procedure into the automata-theoretic approach to model-checking to define new model-checking algorithms for pushdown systems against both linear and branching-time properties. From these results we derive upper bounds for several model-checking problems as well as matching lower bounds. [Pdf]

  • T. Dang, O. Maler, Reachability Analysis via Face Lifting. In this paper we discuss the problem of calculating the reachable states of a dynamical system defined by ordinary differential equations or inclusions. We present a prototype system for approximating this set and demonstrate some experimental results. [Pdf]

  • E. Asarin, O. Maler, A.Pnueli, On Discretization of Delays in Timed Automata and Digital Circuits. In this paper we solve the following problem: "given a digital circuit composed of gates whose real-valued delays are in an integer-bounded interval, is there a way to discretize time while preserving the qualitative behavior of the circuit?" This problem is described as open in [Brzozowski and Seger]. When "preservation of qualitative behavior" is interpreted in a strict sense, as having all original sequences of events with their original ordering we obtain the following two results: 1) For acyclic (combinatorial) circuits whose inputs change only once, the answer is positive: there is a constant $\d$, depending on the maximal number of possible events in the circuit, such that if we restrict all events to take place at multiples of $\d$, we still preserve qualitative behaviors. 2) For cyclic circuits the answer is negative: a simple circuit with three gates can demonstrate a qualitative behavior which cannot be captured by any discretization. Nevertheless we show that a weaker notion of preservation, similar to that of [Henzinger Manna and Pnueli], allows in many cases to verify discretized circuits with $\d=1$ such that the verification results are valid in dense time. [Pdf]

  • E. Asarin, O. Maler, A.Pnueli, J. Sifakis, Controller Synthesis for Timed Automata. In this work we tackle the following problem: given a timed automaton, restrict its transition relation in a systematic way so that all the remaining behaviors satisfy certain properties. This is an extension of the problem of controller synthesis for discrete event dynamical systems, where in addition to choosing among actions, the controller have the option of doing nothing and let the time pass. The problem is formulated using the notion of a real-time game, and a winning strategy is constructed as a fixed-point of an operator on the space of states and clock configurations. [Pdf]

  • O. Maler, A Unified Approach for Studying Discrete and Continuous Dynamical Systems. The goal of this paper is to present discrete transition systems and continuous dynamical systems in a uniform manner, stressing the fundamental differences as well as the commonalities between these two fundamental models. Such a framework seems to be a pre-requisite to any theory and methodology for hybrid systems. For both types of systems we introduce three models (a closed system, a system with one type of input and a system with two types of input) such that the problems associated with them correspond respectively to the tasks of simulation, verification and control synthesis. We will discuss some of the computational problems associated with building control CAD tools that carry these tasks. [Pdf]

  • O. Bournez, O. Maler, A. Pnueli, Orthogonal Polyhedra: Representation and Computation. In this paper we investigate orthogonal polyhedra, i.e. polyhedra which are finite unions of full-dimensional hyper-rectangles. We define representation schemes for these polyhedra based on their vertices, and show that these compact representation schemes are canonical for all (convex and non-convex) polyhedra in any dimension. We then develop efficient algorithms for membership, face-detection and Boolean operations for these representations. [Pdf]

  • E. Asarin, O. Maler, As Soon as Possible: Time Optimal Control for Timed Automata. In this work we tackle the following problem: given a timed automaton, and a target set F of configurations, restrict its transition relation in a systematic way so that from every state, the remaining behaviors reach F as soon as possible. This consists in extending the controller synthesis problem for timed automata, solved in [MPS95,AMPS98], to deal with quantitative properties of behaviors. The problem is formulated using the notion of a timed game automaton, and an optimal strategy is constructed as a fixed-point of an operator on the space of value functions defined on state-clock configurations. [Pdf]

  • M. Bozga, O. Maler, On the Representation of Probabilities over Structured Domains. In this paper we extend one of the main tools used in verification of discrete systems, namely Binary Decision Diagrams (BDD), to treat probabilistic transition systems. We show how probabilistic vectors and matrices can be represented canonically and succinctly using probabilistic trees and graphs, and how simulation of large-scale probabilistic systems can be performed. We consider this work as an important contribution of the verification community to numerous domains which need to manipulate very large matrices. [Pdf]

  • M. Bozga, O. Maler, S. Tripakis Efficient Verification of Timed Automata using Dense and Discrete Time Semantics. In this paper we argue that the semantic issues of {\em discrete} vs.\ {\em dense} time should be separated as much as possible from the pragmatics of state-space representation. Contrary to some misconceptions, the discrete semantics is not inherently bound to use state-explosive techniques any more than the dense one. In fact, discrete timed automata can be analyzed using any representation scheme (such as DBM) used for dense time, and in addition can benefit from enumerative and symbolic techniques (such as BDDs) which are not naturally applicable to dense time. DBMs, on the other hand, can still be used more efficiently by taking into account the {\em activity} of clocks, to eliminate redundancy. To support these claims we report experimental results obtained using an extension of Kronos with BDDs and variable-dimension DBMs where we verified the asynchronous chip STARI, a FIFO buffer which provides for skew-tolerant communication between two synchronous systems. Using discrete time and BDDs we were able to prove correctness of a STARI implementation with 18 stages (55 clocks), better than what has been achieved using other techniques. The verification results carry over to the dense semantics. Using variable-dimension DBMs we have managed to verify STARI for up to 8 stages (27 clocks). In fact, our analysis shows that at most one third of the clocks are active at any reachable state, and about one fourth of the clocks are active in 90\% of the reachable states. These results explain perhaps the reduction achieved using BDDs. [Pdf]

  • E. Asarin, O. Bournez, T. Dang, O. Maler Approximate Reachability Analysis of Piecewise-Linear Dynamical Systems. In this paper we describe an experimental system called d/dt for approximating reachable states for hybrid systems whose continuous dynamics is defined by linear differential equations. We use an approximation algorithm whose accumulation of errors during the continuous evolution is much smaller than in previously-used methods. The d/dt system can, so far, treat non-trivial continuous systems, hybrid systems, convex differential inclusions and controller synthesis problems. [Pdf]

  • O. Bournez, O. Maler, On the Representation of Timed Polyhedra. In this paper we investigate timed polyhedra, i.e. polyhedra which are finite unions of full dimensional simplices of a special kind. Such polyhedra form the basis of timing analysis and in particular of verification tools based on timed automata. We define a representation scheme for these polyhedra based on their extreme vertices, and show that this compact representation scheme is canonical for all (convex and non-convex) polyhedra in any dimension. We then develop relatively efficient algorithms for membership, boolean operations, projection and passage of time for this representation. [Pdf]

  • E. Asarin, S. Bansal, T. Dang, B. Espiau, O. Maler, On Hybrid Control of Under-actuated Mechanical Systems. In this work we present a novel control design methodology for under-actuated mechanical systems. As part of the design process we use the reachability analysis tool d/dt to see whether there is a switching sequence which can drive the system to a desired periodic orbit. Much of the work in the design of the control law is done manually using classical control techniques (unlike the fully-automatic approach advocated in [ABDMP00] and d/dt is used to complement these techniques. We hope this work will contribute to the proliferation of reachability-based techniques to the control engineer's tool box. [Pdf]

  • Y. Abdeddaïm O.Maler, Job-Shop Scheduling using Timed Automata. In this paper we show how the classical job-shop scheduling problem (as well as many other scheduling problem) can be modeled as a special class of acyclic timed automata. Finding an optimal schedule corresponds, then, to finding a shortest (in terms of elapsed time) path in the timed automaton. This representation provides new techniques for solving the optimization problem and, more importantly, it allows to model naturally more complex dynamic resource allocation problems which are not captured so easily in traditional models of operation research. We present several algorithms and heuristics for finding the shortest paths in timed automata and test their implementation in the tool Kronos on numerous benchmark examples. [Pdf]

  • Y. Abdeddaïm, O. Maler,
    • Preemptive Job-Shop Scheduling using Stopwatch Automata. In this paper we show how the problem of job-shop scheduling where the jobs are preemptible can be modeled naturally as a shortest path problem defined on an extension of timed automata, namely stopwatch automata where some of the clocks might be freezed at certain states. Although standard verification problems on stopwatch automata are known to be undecidable, we show that due to well-known properties of optimal schedules, the shortest path in the automaton belongs to a finite class of acyclic paths where transitions occur at integer points in time, and hence the problem is solvable. We present several algorithms and heuristics for finding the shortest paths in such automata and test their implementation on numerous benchmark examples. [Pdf]

  • M. Bozga, H. Jianmin, O. Maler S. Yovine, Verification of Asynchronous Circuits using Timed Automata. In this work we apply the timing verification tool OpenKronos, which is based on timed automata, to verify correctness of numerous asynchronous circuits. The desired behavior of these circuits is specified in terms of signal transition graphs (STG) and we check whether the synthesized circuits behave correctly under the assumption that the inputs satisfy the STG conventions and that the gate delays are bounded between two given numbers. Our results demonstrate the viability of the timed automaton approach for timing analysis of certain classes of circuits. [Pdf]
  • B. Krogh, O. Maler, M. Mahfoudh,
    • On Control with Bounded Computational Resources. In this paper we propose models that capture the influence of computation on the performance of computer-controlled systems, and which allow to employ computational considerations in early stages of the design process of such systems. The problem of whether it is possible to meet performance requirements given resource constraints is phrased as a problem of synthesizing switching controllers for hybrid automata, for which we give algorithms that in some cases are guaranteed to converge and in others can be solved in an approximate manner. [Pdf]

  • P. Niebert, M. Mahfoudh, E. Asarin, M. Bozga, N. Jain, O. Maler,
    • Verification of Timed Automata  via Satisfiability Checking. In this paper we show how to translate bounded-length verification problems for timed automata into formulae in difference logic, a propositional logic enriched with timing constraints. We report some preliminary experiments with a satisfiability checker we have developed for this logic. [Pdf]

  • Y. Abdeddaïm, E. Asarin, O. Maler
    • On Optimal Scheduling under Uncertainty. In this work we treat the problem of scheduling under two types of temporal uncertainty, set-based and probabilistic. For the former we define appropriate optimality criteria and develop an algorithm for finding optimal scheduling strategies using a backward reachability algorithm for timed automata. For probabilistic uncertainty we define and solve a special case of continuous-time Markov Decision Process. All results have been implemented and we provide a preliminary assessment of the merits of each approach. [Pdf]

  • Y. Abdeddaïm, A. Kerbaa, O. Maler  Task Graph Scheduling using Timed Automata. In this paper we develop a methodology for treating the problem of scheduling partially-ordered tasks on parallel machines. Our framework is based on the timed automaton model, originally developed for verification of real-time programs and digital circuits and more recently adapted for solving time-optimal scheduling problems. In this framework, the scheduling problem admits a state-space representation and an optimal schedule corresponds to a shortest path in the timed automaton. We check our implementation on numerous benchmarks and show how release times and deadlines can be easily incorporated into the model. [Pdf]

  • B. Krogh, J. Kapinski, O.Maler, O. Stursberg
    • On Systematic Simulation of Open Continuous Systems. In this paper we investigate a new technique to determine whether an open continuous system behaves correctly for all admissible input signals. This technique is based on a discretization of the set of possible input signals, and on storing neighborhoods of points reachable by trajectories induced by those signals. Alternatively, this technique, inspired by automata theory, can be seen as an attempt to make simulation a more systematic activity by finding a small set of input signals such that the behaviors they induce ``cover'' the whole reachable state space. [Pdf]

  • R. Ben Salah, M. Bozga, O.Maler
    • On Timing Analysis of Combinational Circuits In this paper we report some progress in applying timed automata technology to large-scale problems. We focus on the problem of finding maximal stabilization time for combinational circuits whose inputs change only once and hence they can be modeled using acyclic timed automata. We develop a ``divide-and-conquer'' methodology based on decomposing the circuit into sub-circuits and using timed automata analysis tools to build conservative low-complexity approximations of the sub-circuits to be used as inputs for the rest of the system. Some preliminary results of this methodology are reported. [Pdf]

  • O. Maler, A. Pnueli, On Recognizable Timed Languages.
    In this work we generalize the fundamental notion of recognizability from untimed to timed languages. The essence of our definition is the existence of a right-morphism from the monoid of timed words into a bounded subset of itself. We show that the recognizable languages are exactly those accepted by deterministic timed automata and argue that this is the right class of timed languages, and that the closure of untimed regular languages under projection is a positive accident that cannot be expected to hold beyond the finite-state case. [Pdf]

  • S. Cotton, E. Asarin, O. Maler, P. Niebert, Some Progress in Satisfiability Checking for Difference Logic
    In this paper we report a new SAT solver for difference logic, a propositional logic enriched with timing constraints. The main novelty of our solver is a tighter integration of the incremental analysis of numerical conflicts with the process of boolean conflict analysis. This and other improvements lead to significant performance gains for some classes of problems. [Pdf]

  • O. Maler, D. Nickovic, Monitoring Temporal Properties of Continuous Signals
    In this paper we introduce a variant of temporal logic tailored for specifying desired properties of continuous signals. The logic is based on a bounded subset of the real-time logic MITL, augmented with a static mapping from continuous domains into propositions. From formulae in this logic we create automatically property monitors that can check whether a given signal of bounded length and finite variability satisfies the property. A prototype implementation of this procedure was used to check properties of simulation traces generated by Matlab/Simulink. [Pdf]

  • T. Dang, A. Donze, O. Maler, Verification of Analog and Mixed Signal Circuits using Hybrid Systems Techniques
    In this paper we demonstrate a potential extension of formal verification methodology in order to deal with analog and mixed-signal circuits. In particular, we focus on verifying time-domain properties. The time-dependent behavior of an analog circuit can be described by a system of differential algebraic equations. To model and analyse such circuits under all possible input signals and all values of parameters, we apply various techniques developed in the context of hybrid (discrete- continuous) control systems. First, we extend dense-time reachability analysis and apply it in the case of a biquad lowpass filter. Then, an important mixed-signal circuit, the sigma-delta modulator, is modelised with a discrete-time hybrid system and its stability is analysed using techniques based on mixed integer linear programming. [PDF]

  • M. Bozga, A. Kerbaa, O. Maler, Scheduling Acyclic Branching Programs on Parallel Machines
    [PDF]

  • O. Maler, On Optimal and Sub-optimal Control in the Presence of Adversaries
    This paper constitutes a sketch of a unified framework for posing and solving problems of optimal control in the presence of uncontrolled disturbances. After laying down the general framework we look closely at a concrete instance where the controller is a scheduler and the disturbances are related to uncertainties in task durations. [PS]

  • G. Frehse, B. Krogh, R. Rutenbar, O. Maler, Time Domain Verification of Oscillator Circuit Properties
    The application of formal methods to analog and mixed signal circuits requires efficient methods for constructing abstractions of circuit behaviors. This paper con- cerns the verification of properties of oscillator circuits. Generic monitor automata are proposed to facilitate the application of hybrid system reachability computa- tions to characterize time domain features of oscillatory behavior, such as bounds on the signal amplitude and jitter. The approach is illustrated for a nonlinear tunnel-diode circuit model using PHAVer, a hybrid system analysis tool that pro- vides sound verification results based on linear hybrid automata approximations and infinite precision computations. [PDF]

  • O. Maler, D. Nickovic, A. Pnueli, Real Time Temporal Logic: Past, Present, Future
    This paper attempts to improve our understanding of timed languages and their relation to timed automata. We start by giving a constructive proof of the folk theorem stating that timed languages specified by the past fragment of MITL, can be accepted by deterministic timed automata. On the other hand we provide a proof that certain languages expressed in the future fragment of MITL are not deterministic, and analyze the reason for this asymmetry. [PDF]

  • O. Maler Analog Circuit Verification: a State of an Art
    Extending formal verification methodology toward analog circuits is a very challenging task that will occupy researchers for some time. To put this challenge in context we sketch some of the history of digital circuit verification as well as more recent attempts to adapt it to continnuous and hybrid systems. [PDF]

  • A. Girard, C. Le Guernic, O. Maler, Efficient Computation of Reachable Sets of Linear Time-Invariant Systems with Inputs
    This work is concerned with the problem of computing the set of reachable states for linear time-invariant systems with bounded inputs. Our main contribution is a novel algorithm which improves significantly the computational complexity of reachability analysis. Algorithms to compute over and under-approximations of the reachable sets are proposed as well. These algorithms are not subject to the {\it wrapping effect} and therefore our approximations are {\it tight}. We show that these approximations are useful in the context of hybrid systems verification and control synthesis. The performance of a prototype implementation of the algorithm confirms its qualities and gives hope for scaling up verification technology for continuous and hybrid systems. [PDF]

  • S. Cotton, O. Maler Fast and Flexible Difference Constraint Propagation for DPLL(T)
    In the context of DPLL(T), theory propagation is the process of dynamically selecting consequences of a conjunction of constraints from a given set of candidate constraints. We present improvements to a fast theory propagation procedure for difference constraints of the form x-y=c. These improvements are demonstrated experimentally. [PDF]

  • R. Ben Salah, M. Bozga, O. Maler, On Interleaving in Timed Automata
    We propose a remedy to that part of the state-explosion problem for timed automata which is due to interleaving of actions. We prove the following quite surprising result: the union of all zones reached by different interleavings of the same set of transitions is {\em convex}. Consequently we can improve the standard reachability computation for timed automata by merging such zones whenever they are encountered. Since passage of time distributes over union, we can continue the successor computation from the new zone and eliminate completely the explosion due to interleaving. [PDF]

  • O. Maler, D. Nickovic, A. Pnueli, From MITL to Timed Automata
    We show how to transform formulae written in the real-time temporal logic MITL into timed automata that recognize their satisfying models. This compositional construction is much simpler than previously known and can be easily implemented. [PDF]