On the Length and Depth of Temporal Formulae Distinguishing Non-bisimilar Transition Systems

Goranko, Valentin and Kuijer, Louwe B ORCID: 0000-0001-6696-9023 (2016) On the Length and Depth of Temporal Formulae Distinguishing Non-bisimilar Transition Systems. In: 2016 23rd International Symposium on Temporal Representation and Reasoning (TIME), 2016-10-17 - 2016-10-19.

Text PID4398105.pdf - Author Accepted Manuscript Download (307kB)

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.

Item Type:	Conference or Workshop Item (Unspecified)
Depositing User:	Symplectic Admin
Date Deposited:	04 Dec 2018 09:42
Last Modified:	15 Mar 2024 04:42
DOI:	10.1109/time.2016.26
Related URLs:	Publisher
URI:	https://livrepository.liverpool.ac.uk/id/eprint/3029212