By Neda Saeedloei,
University of Texas
December 2011
Abstract
There has been a tremendous amount of work on incorporation of time in computation for modeling and implementing real-time systems. Most efforts incorporate time by discretizing it. Discretizing means that time is represented through finite time intervals. As a result, infinitesimally small time intervals cannot be represented or reasoned about in these approaches. In practical real-time systems, e.g., a nuclear reactor, two or more events can occur within an infinitesimally small interval. In this dissertation, we develop techniques for including continuous time in computations. These techniques result in frameworks for modeling and verification of real-time systems. Our proposed framework is based on logic programming (LP) extended with constraints and coinduction. To build the theoretical foundations necessary for this work, we present a new programming paradigm, co-constraint logic programming (co-CLP for brevity), that merges two programming paradigms: constraint logic programming and coinductive logic programming. Constraint logic programming (CLP) has been proposed as a declarative paradigm for merging constraint solving and logic programming. Coinductive logic programming, on the other hand, has been proposed as a powerful extension of logic programming for handling infinite (rational) objects and reasoning about their properties. Since CLP’s declarative semantics is given in terms of a least fixed-point, i.e., it is inductive, it cannot be directly used for reasoning about infinite and cyclical objects and their properties. Coinductive logic programming does not include constraints. Co-CLP combines both constraint logic programming and coinduction and enables us to reason about infinite (rational) structures in the presence of constraints.
In this dissertation, we investigate incorporation of continuous time in various domains of computer science. In particular we study the extension of ω-grammars with continuous time (timed ω-grammars) and also continuous time extension of π-calculus (timed π-calculus). We present the implementation of these formalisms in co-CLP and show how these co-CLP- based realization can be used for modeling and verifying real-time systems. We also present a co-CLP framework for modeling hybrid automata, of which pushdown timed automata and timed automata are instances; we use this logic programming realization of hybrid automata to develop a framework for modeling and verification of cyber-physical systems, including real-time systems.