Automata constructions and decision procedures for metric temporal logic

Abstract

Linear-Time Temporal Logic (LTL) [Pnu77] and its timed variant Metric Temporal Logic (MTL) [Koy90] are popular ways of specifying and reasoning about qualitative and quantitative behaviours of systems. In this thesis, we propose some automata-based constructions and decision procedures for LTL and MTL. We describe below the main contributions in this thesis. An important problem associated with LTL is its verification problem. At the heart of the solution for this problem lies the construction of a formula automaton for the given formula. In this thesis, we present a construction of a monitoring automaton for an LTL formula in the framework of “hierarchical Büchi automata” (HBA’s). Though our constructions are similar in spirit to that of Kesten and Pnueli [KP05], our constructions are more concise, using an optimal number of states and transitions. Metric Interval Temporal Logic (MITL), introduced by Alur et al. in [AFH96], is a popularly used logic for specifying quantitative timing properties of real-time systems. The key to solving the satisfiability and verification problem for MITL is the construction of the formula automaton for MITL formulas. In this thesis, we propose a formula automaton construction based on the inductive construction given by Maler et al. in [MNP06]. However, our construction differs from [MNP06] in some key aspects. Firstly, our constructions are more efficient in the usage of clocks as they could potentially use one clock less than the earlier constructions given in [AFH96, MNP06] for O/ and subformulas. Secondly, we prove that our constructions are clock-optimal for the formulas and where ? is an action. Thirdly, our technique is more general as it handles the full fragment of MITL and not just closed intervals as done in [MNP06]. We also give a proof of correctness of our construction. Finally, we formalize the communication link among the automata in terms of what we call “Hierarchical Timed Büchi Automaton” that facilitates the inductive construction of monitoring automata. The satisfiability problem for MITL is also important as it is closely related to the model checking problem for the logic. In this thesis, we give a number of satisfiability-preserving translations for different fragments of MTL which have a direct bearing on the decidability of the satisfiability problem for these logics. Among our results includes a satisfiability-preserving translation for eliminating Si subformulas from any given MITL formula. The notion of a “conflict-tolerant” specification was proposed in [DG08, DGRS08] as a way of specifying controllers which are intermittently in control of a system. An important component missing in the framework of [DG08, DGRS08] is the ability to specify conflict-tolerant specifications in a specification language like temporal logic. We fill this gap in the domain of real-time systems, by proposing a logic called “conflict-tolerant MITL” (CT-MITL) as a way of specifying conflict-tolerant specifications in MITL. We show how to solve the associated verification problem and synthesis problem for CT-MITL using our HTBA-based monitoring automata construction for MITL. We conclude by showing how to synthesize a conflict-tolerant controller in SIMULINK using simple off-the-shelf “delay” and “pulse” blocks.