School of Computing

Modeling Decentralized Real-Time Control by State Space Partition of Timed Automata

Thanikesavan Sivanthi, Srivas Chennu, and Lothar Kreft

In DS-RT '05: Proceedings of the Ninth IEEE International Symposium on Distributed Simulation and Real-Time Applications, pages 182-196. IEEE Computer Society, October 2005.

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.

Download publication 207 kbytes

Bibtex Record

@inproceedings{2484,
author = {Thanikesavan Sivanthi and Srivas Chennu and Lothar Kreft},
title = {{M}odeling {D}ecentralized {R}eal-{T}ime {C}ontrol by {S}tate {S}pace {P}artition of {T}imed {A}utomata},
month = {October},
year = {2005},
pages = {182-196},
keywords = {determinacy analysis, Craig interpolants},
note = {},
doi = {},
url = {http://www.cs.kent.ac.uk/pubs/2005/2484},
    publication_type = {inproceedings},
    submission_id = {21131_1171315531},
    ISBN = {0-7695-2462-1},
    booktitle = {DS-RT '05: Proceedings of the Ninth IEEE International Symposium on Distributed Simulation and Real-Time Applications},
    publisher = {IEEE Computer Society},
}

School of Computing, University of Kent, Canterbury, Kent, CT2 7NF

Enquiries: +44 (0)1227 824180 or contact us.

Last Updated: 21/03/2014