A Logic with Reverse Modalities for History-preserving Bisimulations
We introduce event identifier logic (EIL) which extends Hennessy-Milner logic by the addition of (1) reverse as well as forward modalities, and (2) identifiers to keep track of events. We show that this logic corresponds to hereditary history-preserving (HH) bisimulation equivalence within a particu...
| Main Authors: | , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Open Publishing Association
2011-08-01
|
| Series: | Electronic Proceedings in Theoretical Computer Science |
| Online Access: | http://arxiv.org/pdf/1108.4470v1 |
| _version_ | 1818937964960415744 |
|---|---|
| author | Irek Ulidowski Iain Phillips |
| author_facet | Irek Ulidowski Iain Phillips |
| author_sort | Irek Ulidowski |
| collection | DOAJ |
| description | We introduce event identifier logic (EIL) which extends Hennessy-Milner logic by the addition of (1) reverse as well as forward modalities, and (2) identifiers to keep track of events. We show that this logic corresponds to hereditary history-preserving (HH) bisimulation equivalence within a particular true-concurrency model, namely stable configuration structures. We furthermore show how natural sublogics of EIL correspond to coarser equivalences. In particular we provide logical characterisations of weak history-preserving (WH) and history-preserving (H) bisimulation. Logics corresponding to HH and H bisimulation have been given previously, but not to WH bisimulation (when autoconcurrency is allowed), as far as we are aware. We also present characteristic formulas which characterise individual structures with respect to history-preserving equivalences. |
| first_indexed | 2024-12-20T06:00:20Z |
| format | Article |
| id | doaj.art-8fd6494fa27c4528b007f6e6525e71e9 |
| institution | Directory Open Access Journal |
| issn | 2075-2180 |
| language | English |
| last_indexed | 2024-12-20T06:00:20Z |
| publishDate | 2011-08-01 |
| publisher | Open Publishing Association |
| record_format | Article |
| series | Electronic Proceedings in Theoretical Computer Science |
| spelling | doaj.art-8fd6494fa27c4528b007f6e6525e71e92022-12-21T19:50:55ZengOpen Publishing AssociationElectronic Proceedings in Theoretical Computer Science2075-21802011-08-0164Proc. EXPRESS 201110411810.4204/EPTCS.64.8A Logic with Reverse Modalities for History-preserving BisimulationsIrek UlidowskiIain PhillipsWe introduce event identifier logic (EIL) which extends Hennessy-Milner logic by the addition of (1) reverse as well as forward modalities, and (2) identifiers to keep track of events. We show that this logic corresponds to hereditary history-preserving (HH) bisimulation equivalence within a particular true-concurrency model, namely stable configuration structures. We furthermore show how natural sublogics of EIL correspond to coarser equivalences. In particular we provide logical characterisations of weak history-preserving (WH) and history-preserving (H) bisimulation. Logics corresponding to HH and H bisimulation have been given previously, but not to WH bisimulation (when autoconcurrency is allowed), as far as we are aware. We also present characteristic formulas which characterise individual structures with respect to history-preserving equivalences.http://arxiv.org/pdf/1108.4470v1 |
| spellingShingle | Irek Ulidowski Iain Phillips A Logic with Reverse Modalities for History-preserving Bisimulations Electronic Proceedings in Theoretical Computer Science |
| title | A Logic with Reverse Modalities for History-preserving Bisimulations |
| title_full | A Logic with Reverse Modalities for History-preserving Bisimulations |
| title_fullStr | A Logic with Reverse Modalities for History-preserving Bisimulations |
| title_full_unstemmed | A Logic with Reverse Modalities for History-preserving Bisimulations |
| title_short | A Logic with Reverse Modalities for History-preserving Bisimulations |
| title_sort | logic with reverse modalities for history preserving bisimulations |
| url | http://arxiv.org/pdf/1108.4470v1 |
| work_keys_str_mv | AT irekulidowski alogicwithreversemodalitiesforhistorypreservingbisimulations AT iainphillips alogicwithreversemodalitiesforhistorypreservingbisimulations AT irekulidowski logicwithreversemodalitiesforhistorypreservingbisimulations AT iainphillips logicwithreversemodalitiesforhistorypreservingbisimulations |