Automata based abstraction of interval assumptions and bounded input linear systems for verification and controller synthesis

Abstract

Verification of general reachability conditions and controller synthesis satisfying the same can be efficiently performed on finite state automata and timed automata. As such, a standard technique for verification and controller synthesis on non-automata specifications is to abstract the specifications as finite state automata or timed automata. In this thesis, we extend the paradigm of automata based abstraction in the following two directions: • A subset of timed computational tree logic (TCTL), called interval assumptions, is abstracted as a type of timed automata called continuous pure signal input output automata. This abstraction is done for verifying guarantees (or requirements) specified in TCTL for timed automata under environments specified as interval assumptions. The approach is useful for modular verification of manufacturing systems, standard small scale examples of which include the Turntable and Production Cell. This is the first attempt to use a subset of TCTL as assumptions in modular verification. • Near-complete abstraction of bounded input linear control systems as finite state metric transition systems. Near-completeness is a parametrized notion of completeness of an abstraction, introduced in this thesis. The abstraction as a finite state metric transition system allows controller synthesis to be performed on the finite state automaton corresponding to the finite state metric transition system. The novel contributions of this work are defining near-completeness and building near-complete models of bounded input possibly unstable linear control systems. Hitherto approaches for complete abstraction either considered stable systems, or else unstable but unbounded input systems. We extend the extant approaches to unstable plus bounded input systems, while replacing the completeness criterion with the near-completeness criterion.