Document Open Access Logo

Precongruence Formats with Lookahead through Modal Decomposition

Authors Wan Fokkink, Rob J. van Glabbeek

PDF
Thumbnail PDF

File

LIPIcs.CSL.2017.25.pdf
  • Filesize: 0.51 MB
  • 20 pages

Document Identifiers

Author Details

Wan Fokkink
Rob J. van Glabbeek

Cite AsGet BibTex

Wan Fokkink and Rob J. van Glabbeek. Precongruence Formats with Lookahead through Modal Decomposition. In 26th EACSL Annual Conference on Computer Science Logic (CSL 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 82, pp. 25:1-25:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
https://doi.org/10.4230/LIPIcs.CSL.2017.25

Abstract

Bloom, Fokkink & van Glabbeek (2004) presented a method to decompose formulas from Hennessy-Milner logic with regard to a structural operational semantics specification. A term in the corresponding process algebra satisfies a Hennessy-Milner formula if and only if its subterms satisfy certain formulas, obtained by decomposing the original formula. They used this decomposition method to derive congruence formats in the realm of structural operational semantics. In this paper it is shown how this framework can be extended to specifications that include bounded lookahead in their premises. This extension is used in the derivation of a congruence format for the partial trace preorder.
Keywords
  • Structural Operational Semantics
  • Compositionality
  • Congruence
  • Modal Logic
  • Modal Decomposition
  • Lookahead

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. P. America and J. W. de Bakker. Designing equivalent semantic models for process creation. Theoretical Computer Science, 60(2):109-176, 1988. URL: http://dx.doi.org/10.1016/0304-3975(88)90048-5.
  2. J. C. M. Baeten and F. W. Vaandrager. An algebra for process creation. Acta Informatica, 29(4):303-334, 1992. URL: http://dx.doi.org/10.1007/BF01178776.
  3. Marco Bernardo. Enriching empa with value passing: A symbolic approach based on lookahead. In Proc. PAPM 1997, pages 35-49, 1997. Google Scholar
  4. B. Bloom. When is partial trace equivalence adequate? Formal Aspects of Computing, 6(3):317-338, 1994. URL: http://dx.doi.org/10.1007/BF01215409.
  5. B. Bloom, W. J. Fokkink, and R. J. van Glabbeek. Precongruence formats for decorated trace semantics. Transactions on Computational Logic, 5(1):26-78, 2004. URL: http://dx.doi.org/10.1145/963927.963929.
  6. B. Bloom, S. Istrail, and A. R. Meyer. Bisimulation can't be traced. Journal of the ACM, 42(1):232-268, 1995. URL: http://dx.doi.org/10.1145/200836.200876.
  7. R. Bol and J. F. Groote. The meaning of negative premises in transition system specifications. Journal of the ACM, 43(5):863-914, 1996. URL: http://dx.doi.org/10.1145/234752.234756.
  8. V. Castiglioni, D. Gebler, and S. Tini. Modal decomposition on nondeterministic probabilistic processes. In Proc. CONCUR 2016, volume 59 of LIPIcs, pages 36:1-36:15. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2016. URL: http://dx.doi.org/10.4230/LIPIcs.CONCUR.2016.36.
  9. P. R. D'Argenio and M. D. Lee. Probabilistic transition system specification: Congruence and full abstraction of bisimulation. In Proc. FOSSACS 2012, volume 7213 of LNCS, pages 452-466. Springer, 2012. URL: http://dx.doi.org/10.1007/978-3-642-28729-9_30.
  10. A. J. Dos Reis. Compiler Construction Using Java, JavaCC, and Yacc. Wiley-IEEE, 2012. URL: http://dx.doi.org/10.1002/9781118112762.
  11. W. J. Fokkink and R. J. van Glabbeek. Ntyft/ntyxt rules reduce to ntree rules. Information and Computation, 126(1):1-10, 1996. URL: http://dx.doi.org/10.1006/inco.1996.0030.
  12. W. J. Fokkink and R. J. van Glabbeek. Divide and congruence II: Delay and weak bisimilarity. In Proc. LICS 2016, pages 778-787. ACM/IEEE, 2016. URL: http://dx.doi.org/10.1145/2933575.2933590.
  13. W. J. Fokkink, R. J. van Glabbeek, and P. de Wind. Compositionality of Hennessy-Milner logic by structural operational semantics. Theoretical Computer Science, 354(3):421-440, 2006. URL: http://dx.doi.org/10.1016/j.tcs.2005.11.035.
  14. W. J. Fokkink, R. J. van Glabbeek, and P. de Wind. Divide and congruence: From decomposition of modal formulas to preservation of branching and η-bisimilarity. Information and Computation, 214:59-85, 2012. URL: http://dx.doi.org/10.1016/j.ic.2011.10.011.
  15. R. J. van Glabbeek. Full abstraction in structural operational semantics (extended abstract). In Proc. AMAST 1993, Workshops in Computing, pages 75-82. Springer, 1993. URL: http://dx.doi.org/10.1007/978-1-4471-3227-1_7.
  16. R. J. van Glabbeek. The linear time - branching time spectrum I: The semantics of concrete, sequential processes. In J. A. Bergstra, A. Ponse, and S. A. Smolka, editors, Handbook of Process Algebra, chapter 1, pages 3-99. Elsevier, 2001. Google Scholar
  17. R. J. van Glabbeek. On cool congruence formats for weak bisimulations. Theoretical Computer Science, 412(28):3283-3302, 2011. URL: http://dx.doi.org/10.1016/j.tcs.2011.02.036.
  18. J. F. Groote and F. Vaandrager. Structured operational semantics and bisimulation as a congruence. Information and Computation, 100(2):202-260, 1992. URL: http://dx.doi.org/10.1016/0890-5401(92)90013-6.
  19. M. Hennessy and R. Milner. Algebraic laws for nondeterminism and concurrency. Journal of the ACM, 32(1):137-161, 1985. URL: http://dx.doi.org/10.1145/2455.2460.
  20. K. V. Hindriks and M. B. van Riemsdijk. Satisfying maintenance goals. In Proc. DALT 2007, volume 4897 of LNCS, pages 86-103. Springer, 2007. URL: http://dx.doi.org/10.1007/978-3-540-77564-5_6.
  21. K. G. Larsen. Context-Dependent Bisimulation between Processes. PhD thesis, University of Edinburgh, 1986. Google Scholar
  22. L. Léonard and G. Leduc. A formal definition of time in LOTOS. Formal Aspects of Computing, 10(3):248-266, 1998. URL: http://dx.doi.org/10.1007/s001650050015.
  23. M. R. Mousavi. Causality in the semantics of Esterel: Revisited. In Proc. SOS 2009, volume 18 of EPTCS, pages 32-45, 2009. URL: http://dx.doi.org/10.4204/EPTCS.18.3.
  24. G. D. Plotkin. A structural approach to operational semantics. Journal of Logic and Algebraic Programming, 60-61:17-139, 2004. URL: http://dx.doi.org/10.1016/j.jlap.2004.05.001.
  25. R. de Simone. Higher-level synchronising devices in Meije-SCCS. Theoretical Computer Science, 37(3):245-267, 1985. URL: http://dx.doi.org/10.1016/0304-3975(85)90093-3.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact