Modeling decentralized real-time control by state space partition of timed automata

Author

Sivanthi, Thanikesavan ; Chennu, Srivas ; Kreft, Lothar

Author_Institution

Dept. of Commun. Networks, Hamburg Univ. of Technol., Germany

fYear

2005

fDate

10-12 Oct. 2005

Firstpage

229

Lastpage

235

Abstract

Timed automata provide useful state machine based representations for the validation and verification of realtime control systems. This paper introduces an algorithmic methodology to translate the state space visualization of a centralized real-time control system to a decentralized one. Given a set of timed automata representing a centralized real-time control system, the algorithm partitions them into a collection of interacting submachines. Importantly, this methodology allows for model-checking of the derived decentralized system against the same set of verifications as that specified for the centralized system. The complexity analysis of the algorithm is presented as a function of the number of tasks and nodes comprising the decentralized system.

Keywords

automata theory; computational complexity; decentralised control; formal specification; formal verification; real-time systems; state-space methods; centralized real-time control system; decentralized real-time control; decentralized system; model-checking; realtime control systems; state machine; state space partition; state space visualization; timed automata; Automata; Automatic control; Centralized control; Communication networks; Communication system control; Control system synthesis; Control systems; Partitioning algorithms; Real time systems; State-space methods;

fLanguage

English

Publisher

ieee

Conference_Titel

Distributed Simulation and Real-Time Applications, 2005. DS-RT 2005 Proceedings. Ninth IEEE International Symposium on

Print_ISBN

0-7695-2462-1

Type

conf

DOI

10.1109/DISTRA.2005.28

Filename

1530674