Integrating timed condition/event systems and timed automata for the verification of hybrid systems

Abstract

. In this paper we integrate two different approaches for the specification and verification of timed systems being used in control theory and computer science. These are the timed condition/event systems and the timed automata formalisms. Our main result states that timed condition/event systems can be efficiently transformed into timed automata which then can be analyzed automatically. 1. Introduction. Many computer-controlled systems consist of discrete components interacting with continuously evolving sub-systems. Such systems can be found in avionics, robotics, chemical plants, and other fields. Systems involving discrete as well as continuous or sectionally continuous components are called hybrid systems. A very important sub-class of hybrid systems consists of realtime systems which are systems depending on hard deadlines and on real-time constraints. A typical real-time constraint is that the response time of the controller to some events generated by the controlled components...