2016 23rd International Symposium on Temporal Representation and Reasoning (TIME) (2016)

Kongens Lyngby, Denmark

Oct. 17, 2016 to Oct. 19, 2016

ISSN: 2332-6468

ISBN: 978-1-5090-3825-1

pp: 177-185

DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/TIME.2016.26

ABSTRACT

We investigate the minimal length and nesting depth of temporal formulae that distinguish two given non-bisimilar finite pointed transition systems. We show that such formula can always be constructed in length at most exponential in the combined number of states of both transition systems, and give an example with exponential lower bound, for several common temporal languages. We then show that by using renamings of subformulae or explicit assignments the length of the distinguishing formula can always be reduced to one that is bounded above by a cubic polynomial on the combined size of both transition systems. This is also a bound for the size obtained by using DAG representation of formulae. We also prove that the minimal nesting depth for such formula is less than the combined size of the two state spaces and obtain some tight upper bounds.

INDEX TERMS

Games, Manganese, Atomic measurements, Upper bound, Standards, Electronic mail, Semantics,length and depth of distinguishing formula, non-bisimilar transition systems, temporal logics

CITATION

Valentin Goranko,
Louwe B. Kuijer,
"On the Length and Depth of Temporal Formulae Distinguishing Non-bisimilar Transition Systems",

*2016 23rd International Symposium on Temporal Representation and Reasoning (TIME)*, vol. 00, no. , pp. 177-185, 2016, doi:10.1109/TIME.2016.26