IIIT Hyderabad Publications 


Automata based abstraction of interval assumptions and bounded input linear systems for verification and controller synthesisAuthor: Santosh Arvind Adimoolam Date: 20141008 Report no: IIIT/TH/2014/50 Advisor:Venkatesh Choppella,K Viswanath AbstractVerification 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 nonautomata 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. • Nearcomplete abstraction of bounded input linear control systems as finite state metric transition systems. Nearcompleteness 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 nearcompleteness and building nearcomplete 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 nearcompleteness criterion. Full thesis: pdf Centre for Software Engineering Research Lab 

Copyright © 2009  IIIT Hyderabad. All Rights Reserved. 