English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Zendy Plus

Presents the access of premium content as premium feature

Premium Content

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Zendy Tools

Zendy Open

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.

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