document: Verification of timed automata based on similarity 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 -LRB- state spaces -RRB- 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
doc_bio_tags: O O O O O O O O O O O O O O O B I O O B I I O O O O O O O O O O O O B O O O O O O O O O O O O O O O O O O O O B I O B I I I O O O O O O O O O O O O B I I
extractive_keyphrases: partitioning technique abstract state spaces bisimilarity universal fragments branching time temporal logics observational simulation relations
abstractive_keyphrases: timed automata verification