Oded Maler: Abstracts of Journal Articles

  • B. Delyon, O. Maler, On the Effects of Noise and Speed on Computations.
    In this paper we propose a model that captures the influence of noise and speed on the correct behavior of a computing device situated in a dynamic environment. Within this model we analyze the relation between structural properties of automata and their immunity to noise. We prove upper- and lower-bounds on the effect of noise for various classes of finite automata. In addition we show similar relatinoships between relative speeds of the automaton and the environment and the accuracy of computation. Our model, combining basic notions from algebraic automata theory and the theory of stochastic processes, can serve as a starting point for a rigorous theory of computational systems embedded in the real world. [Pdf]

  • O. Maler, A. Pnueli, On the Learnability of Infinitary Regular Sets.
    In this paper we extend the automaton synthesis paradigm to infinitary languages, that is, to subsets of the set $\S^\o$ of all infinite sequences over some alphabet $\S$. Our main result is a polynomial algorithm for learning a sub-class of the $\o$-regular sets from membership queries and counter-examples based on the framework suggested by Angluin (Angluin, D., 1987, {\it Information and Computation} 75) for learning regular subsets of $\S^*$. [Pdf]

  • A. Asarin, O. Maler, A. Pnueli, Reachability Analysis of Dynamical Systems having Piecewise-Constant Derivatives.
    In this paper we consider a class of hybrid systems, namely dynamical systems with piecewise-constant derivatives (PCD systems). Such systems consist of a partition of the Euclidean space into a finite set of polyhedral sets ({\it regions}). Within each region the dynamics is defined by a constant vector field, hence discrete transitions occur only on the boundaries between regions where the trajectories change their direction.
    With respect to such systems we investigate the reachability question: {\it Given an effective description of the systems and of two polyhedral subsets $P$ and $Q$ of the state-space, is there a trajectory starting at some $\vx \in P$ and reaching some point in $Q$? } Our main results are a decision procedure for two-dimensional systems, and an undecidability result for three or more dimensions. [Pdf]

  • O. Maler, A Decomposition Theorem for Probabilistic Transition Systems.
    In this paper we prove that every finite Markov chain can be decomposed into a cascade product of a Bernoulli process and several simple permutation-reset {\it deterministic} automata. The original chain is a state-homomorphic image of the product. By doing so we give a positive answer to an open question stated in [Paz71] concerning the decomposability of probabilistic systems. Our result is based on the observation that in probabilistic transition systems, ``randomness'' and ``memory'' can be separated so as to allow the non-random part to be treated using common deterministic automata-theoretic techniques. The same separation technique can be applied to other kinds of non-determinism as well. [Pdf]

  • O. Maler, L. Staiger On Syntactic Congruences for Omega-Languages.
    In this paper we investigate several questions related to syntactic congruences and to minimal automata associated with $\omega$-languages. In particular we investigate relationships between the so-called simple (because it is a simple translation from the usual definition in the case of finitary languages) syntactic congruence and its infinitary refinement (the iteration congruence) investigated by Arnold [Ar85]. We show that in both cases not every $\omega$-language having a finite syntactic monoid is regular and we give a characterization of those $\omega$-languages having finite syntactic monoids.
    Among the main results we derive a condition which guarantees that the simple syntactic congruence and Arnold's iteration congruence coincide and show that {\it all} (including infinite-state) $\omega$-languages in the Borel class $F_\s\cap G_\d$ satisfy this condition. We also show that all $\omega$-languages in this class are accepted by their minimal-state automaton --- provided they are accepted by any Muller automaton.
    Finally we develop an alternative theory of recognizability of {$\omega$-languages} by families of right-congruence relations, and define a canonical object (much smaller than the iteration monoid) associated with every $\omega$-language. Using this notion of recognizability we give a necessary and sufficient condition for a regular $\omega$-language to be accepted by its minimal-state automaton. [Pdf]

  • E.Asarin, O. Maler, Achilles and the Tortoise Climbing Up the Arithmetical Hierarchy.
    In this paper we show how to construct for every set R of integers in the arithmetical hierarchy a dynamical system H with piecewise-constant derivatives (PCD) such that deciding membership in R can be reduced to solving the reachability problem between two rational points for H. The ability of such simple dynamical systems to "simulate" highly undecidable problems is closely related to Zeno's paradox dealing with the ability to pack infinitely many discrete steps in a bounded interval of time. [Pdf]

  • E. Asarin, O. Bournez, T. Dang, O. Maler, A. Pnueli, Effective Synthesis of Switching Controllers for Linear Systems.
    In this work we suggest a novel methodology for synthesizing switching controllers for continuous and hybrid systems whose dynamics are defined by linear differential equations. We formulate the synthesis problem as finding the conditions upon which a controller should switch the behavior of the system from one "mode" to another in order to avoid a set of bad states, and propose an abstract algorithm which solves the problem by an iterative computation of reachable states. We have implemented a concrete version of the algorithm, which uses a new approximation scheme for reachability analysis of linear systems. [Pdf]

    • A. Bouajjani, J. Esparza, A. Finkel, O. Maler, P.Rossmanith, B. Willems, P.Wolper, An Efficient Automata Approach to some Problems on Context-free Grammars
    In Chapter 4 of their book "String-Rewriting Systems", Book and Otto solve a number of word problems for monadic string-rewriting systems using an elegant automata-based technique. In this note we observe that the technique is also very interesting from a pedagogical point of view, since it provides a uniform solution to several elementary problems on context-free languages. [Pdf]

  • Y. Kesten, O. Maler, M. Marcus, A. Pnueli, E. Shahar, Symbolic Model Checking with Rich Assertional Languages.
    The paper shows that, by an appropriate choice of a rich assertional language, it is possible to extend the utility of symbolic model checking beyond the realm of BDD-represented finite-state systems into the domain of infinite-state systems, leading to a powerful technique for uniform verification of unbounded (parametrized) process networks. The main contributions of the paper are a formulation of a general framework for symbolic model checking of infinite-state systems, a demonstration that many individual examples of uniformly verified parameterized designs that appear in the literature are special cases of our general approach, extending of the technique to tree architectures and using this extension to verify the correctness of the FutureBus design for all configurations, and establishing that the presented method is a precise dual to the top-down invariant generation method used in deductive verification. [Pdf]

    • E. Asarin, O. Maler, P. Caspi, Timed Regular Expressions
    In this paper we define timed regular expressions, a formalism for specifying discrete behaviors augmented with timing information, and prove that its expressive power is equivalent to the timed automata of Alur and Dill. This result is the timed analogue of Kleene Theorem and, similarly to that result, the hard part in the proof is the translation from automata to expressions. This result is extended from finite to infinite (in the sense of Buchi) behaviors. In addition to these fundamental results, we give a clean algebraic framework for two commonly-accepted formalism for timed behaviors, time-event sequences and piecewise-constant signals. [Pdf]

    O. Maler, Guest Editorial: Verification of Hybrid Systems
    This special issue of The European Journal of Control is dedicated to some of the results of the European Community Esprit-LTR Project 26270 VHS (Verification of Hybrid Systems). It consists of 5 papers dealing with various aspects of one of the case studies treated in the project, the Experimental Batch Plant at the university of Dortmund. Before presenting the papers themselves, it is worthwhile to say something about hybrid systems in general and the VHS project in particular. [Pdf]

  • O. Maler, Control from Computer Science.
    This paper presents some of the principles underlying verification and controller synthesis techniques for discrete dynamical systems developed within Computer Science along with some ideas to extend them to continuous and hybrid systems. Hopefully, this will provide control theorists and engineers with an additional perspective of their discipline as seen by a sympathetic outsider, uncommitted to the customs and traditions of the domain. Inter-cultural experience can be frustrating but sometimes fun. [Pdf]

  • Y. Abdeddaïm, E. Asarin, O. Maler  Scheduling with Timed Automata 
    In this work we present timed automata as a natural tool for posing and solving scheduling problems. We show how efficient shortest path algorithms for timed automata can find optimal schedules for the classical job-shop problem. We then extend these results to synthesize adaptive scheduling strategies for problems with uncertainty in task durations. [Pdf]

  • P. Caspi, O. Maler From Control Loops to Real-Time Programs
    This article discusses what we consider as one of the central aspects of embedded systems: the realization of control systems by software. Although computers are today the most popular medium for implementing controllers, we feel that the state of understanding of this topic is not satisfactory, mostly due to the fact that it is situated in the frontier between two different cultures and world views (control and informatics) which are not easy to reconcile. The purpose of this article is to clarify these issues and present them in a uniform and, hopefully, coherent manner.
    The article is organized as follows. We start with a short high-level discussion of the two phenomena involved, control and computation. In Section 2 we explain the basic issues related to the realization of controllers by software using a simple proportional-integral-derivative (PID) controller as an example. In Section 3 we move to more complex multi-periodic control loops and describe various approaches for scheduling them on a sequential computer. Section 4 is devoted to discrete event (and hybrid) systems and their software implementation. Finally, in Section 5 we briefly discuss distributed control and fault tolerance. [Pdf]