Advertisement

Hereditary History-Preserving Bisimilarity: Logics and Automata

  • Paolo Baldan
  • Silvia Crafa
Part of the Lecture Notes in Computer Science book series (LNCS, volume 8858)

Abstract

We study hereditary history-preserving (hhp-) bisimilarity, a canonical behavioural equivalence in the true concurrent spectrum, by means of logics and automata. We first show that hhp-bisimilarity on prime event structures can be characterised in terms of a simple logic whose formulae just observe events in computations and check their executability. The logic suggests a characterisation of hhp-bisimilarity based on history-dependent automata, a formalism for modelling systems with dynamic allocation and deallocation of resources, where the history of resources is traced over time. Prime event structures can be naturally mapped into history-dependent automata in a way that hhp-bisimilarity exactly corresponds to the canonical behavioural equivalence for history-dependent automata.

Keywords

Free Variable Closed Formula Dynamic Allocation Behavioural Equivalence Logical Characterisation 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    van Glabbeek, R., Goltz, U.: Refinement of actions and equivalence notions for concurrent systems. Acta Informatica 37(4/5), 229–327 (2001)MathSciNetCrossRefzbMATHGoogle Scholar
  2. 2.
    Esparza, J., Heljanko, K.: Unfoldings - A Partial order Approach to Model Checking. EACTS Monographs. Springer (2008)Google Scholar
  3. 3.
    Bednarczyk, M.A.: Hereditary history preserving bisimulations or what is the power of the future perfect in program logics. Technical report, Polish Academy of Sciences (1991)Google Scholar
  4. 4.
    Joyal, A., Nielsen, M., Winskel, G.: Bisimulation from open maps. Information and Computation 127(2), 164–185 (1996)MathSciNetCrossRefzbMATHGoogle Scholar
  5. 5.
    Winskel, G.: Event Structures. In: Brauer, W., Reisig, W., Rozenberg, G. (eds.) APN 1986. LNCS, vol. 255, pp. 325–392. Springer, Heidelberg (1987)Google Scholar
  6. 6.
    Phillips, I., Ulidowski, I.: A hierarchy of reverse bisimulations on stable configuration structures. Mathematical Structures in Computer Science 22(2), 333–372 (2012)MathSciNetCrossRefzbMATHGoogle Scholar
  7. 7.
    Phillips, I., Ulidowski, I.: Reversing algebraic process calculi. Journal of Logic and Algebraic Programming 73(1-2), 70–96 (2007)MathSciNetCrossRefzbMATHGoogle Scholar
  8. 8.
    Cristescu, I., Krivine, J., Varacca, D.: A compositional semantics for the reversible p-calculus. In: Proc. of LICS 2013, pp. 388–397. IEEE Computer Society (2013)Google Scholar
  9. 9.
    Baldan, P., Crafa, S.: A logic for true concurrency. Journal of the ACM 61(4), 24:1–24:36 (2014)Google Scholar
  10. 10.
    Phillips, I., Ulidowski, I.: Event identifier logic. Mathematical Structures in Computer Science 24(2), 1–51 (2014)MathSciNetGoogle Scholar
  11. 11.
    Nielsen, M., Clausen, C.: Games and logics for a noninterleaving bisimulation. Nordic Journal of Computing 2(2), 221–249 (1995)MathSciNetzbMATHGoogle Scholar
  12. 12.
    Hennessy, M., Stirling, C.: The power of the future perfect in program logics. Information and Control 67(1-3), 23–52 (1985)MathSciNetCrossRefzbMATHGoogle Scholar
  13. 13.
    Montanari, U., Pistore, M.: History-Dependent automata: An introduction. In: Bernardo, M., Bogliolo, A. (eds.) SFM-Moby 2005. LNCS, vol. 3465, pp. 1–28. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  14. 14.
    Jurdzinski, M., Nielsen, M., Srba, J.: Undecidability of domino games and hhp-bisimilarity. Information and Computation 184(2), 343–368 (2003)MathSciNetCrossRefzbMATHGoogle Scholar
  15. 15.
    Hennessy, M., Milner, R.: Algebraic laws for nondeterminism and concurrency. Journal of the ACM 32(1), 137–161 (1985)MathSciNetCrossRefzbMATHGoogle Scholar
  16. 16.
    Thiagarajan, P.S.: Regular event structures and finite petri nets: A conjecture. In: Brauer, W., Ehrig, H., Karhumäki, J., Salomaa, A. (eds.) Formal and Natural Computing. LNCS, vol. 2300, pp. 244–256. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  17. 17.
    Vogler, W.: Deciding history preserving bisimilarity. In: Leach Albert, J., Monien, B., Rodríguez-Artalejo, M. (eds.) ICALP 1991. LNCS, vol. 510, pp. 495–505. Springer, Heidelberg (1991)CrossRefGoogle Scholar
  18. 18.
    Montanari, U., Pistore, M.: Minimal transition systems for history-preserving bisimulation. In: Reischuk, R., Morvan, M. (eds.) STACS 1997. LNCS, vol. 1200, pp. 413–425. Springer, Heidelberg (1997)CrossRefGoogle Scholar
  19. 19.
    Fröschle, S., Hildebrandt, T.: On plain and hereditary history-preserving bisimulation. In: Kutyłowski, M., Wierzbicki, T., Pacholski, L. (eds.) MFCS 1999. LNCS, vol. 1672, pp. 354–365. Springer, Heidelberg (1999)CrossRefGoogle Scholar
  20. 20.
    Bojanczyk, M., Klin, B., Lasota, S.: Automata with group actions. In: Proc. of LICS 2011, pp. 355–364. IEEE Computer Society (2011)Google Scholar
  21. 21.
    Prisacariu, C.: The glory of the past and geometrical concurrency. CoRR abs/1206.3136 (2012)Google Scholar

Copyright information

© Springer International Publishing Switzerland 2014

Authors and Affiliations

  • Paolo Baldan
    • 1
  • Silvia Crafa
    • 1
  1. 1.Dipartimento di MatematicaUniversità di PadovaItaly

Personalised recommendations