Reasoning about co-evolving discrete, continuous and hybrid states
Date of Award
Doctor of Philosophy (PhD)
Electrical Engineering and Computer Science
Convergence spaces, Specification logic, Discrete systems, Continuous systems
Computer Sciences | Physical Sciences and Mathematics
In contrast to what we know about controlling, verifying and reasoning about discrete state transition systems and, separately, continuous dynamical systems, we know relatively little about the behavior of even simple hybrid systems, systems consisting of interdependent discrete (e.g. digital) and continuous (e.g analog) components. Logic-based formal techniques are available for discrete systems that enable us to rigorously reason about their evolution over sequences of discrete time. Some of these logics, e.g. S4, have been reinterpreted to act on dynamical systems evolving on continuous time. However, the modeling of hybrid systems has lacked a unified framework that treats both discrete and continuous components of a state in fundamentally the same way. We present a logic for the evolution of hybrid systems in which the notion of time can be discrete, continuous, hybrid or even none of the above. The new logic includes, as special cases, the logics available for discrete and continuous systems.
Rivera G., Angel J., "Reasoning about co-evolving discrete, continuous and hybrid states" (2008). Electrical Engineering and Computer Science - Dissertations. Paper 22.