Verification of Timed Automata Based on Similarity

Issue title: Concurrency Specification and Programming Workshop (CS&P'2001)

Article type: Research Article

Authors: Dembiński, Piotr | Półrola, Agata

Affiliations: Institute of Computer Science, PAS, Ordona 21, 01-237 Warsaw, Poland | Faculty of Mathematics, University of Lodz, Banacha 22, 90-238 Lodz, Poland

Abstract: The paper presents a modification of the standard partitioning technique to generate abstract state spaces preserving similarity for Timed Automata. Since this relation is weaker than bisimilarity, most of the obtained models (state spaces) are smaller than bisimilar ones, but still preserve the universal fragments of branching time temporal logics. The theoretical results are exemplified for strong, delay, and observational simulation relations.

Journal: Fundamenta Informaticae, vol. 51, no. 1-2, pp. 59-89, 2002