Change search
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf
On the Length and Depth of Temporal Formulae Distinguishing Non-bisimilar Transition Systems
Stockholm University, Faculty of Humanities, Department of Philosophy. University of Johannesburg, South Africa.ORCID iD: 0000-0002-0157-1644
2016 (English)In: 23rd International Symposium on Temporal Representation and Reasoning: Proceedings / [ed] Curtis Dyreson, Michael R. Hansen, Luke Hunsberger, IEEE Computer Society, 2016, p. 177-185Conference paper, Published paper (Refereed)
Abstract [en]

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.

Place, publisher, year, edition, pages
IEEE Computer Society, 2016. p. 177-185
Keywords [en]
non-bisimilar transition systems, temporal logics, size of distinguishing formula
National Category
Computer Sciences
Identifiers
URN: urn:nbn:se:su:diva-138309DOI: 10.1109/TIME.2016.26ISBN: 978-1-5090-3825-1 (electronic)OAI: oai:DiVA.org:su-138309DiVA, id: diva2:1066711
Conference
23rd International Symposium on Temporal Representation and Reasoning (TIME'2016), Kongens Lyngby, Denmark, 17–19 October 2016
Funder
Swedish Research Council, 2015-04388Available from: 2017-01-18 Created: 2017-01-18 Last updated: 2018-01-13Bibliographically approved

Open Access in DiVA

fulltext(876 kB)19 downloads
File information
File name FULLTEXT01.pdfFile size 876 kBChecksum SHA-512
251d3c4e330d0e4ace129272d611e7da6d0ab5579799bb6e109241916368ce97eeef5ec042fb6e63a39db6369cf8ce13e45436140ae240cebd156326053b5737
Type fulltextMimetype application/pdf

Other links

Publisher's full text

Search in DiVA

By author/editor
Goranko, Valentin
By organisation
Department of Philosophy
Computer Sciences

Search outside of DiVA

GoogleGoogle Scholar
Total: 19 downloads
The number of downloads is the sum of all downloads of full texts. It may include eg previous versions that are now no longer available

doi
isbn
urn-nbn

Altmetric score

doi
isbn
urn-nbn
Total: 38 hits
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf