On constructibility and unconstructibility of LTS operators from other LTS operators

详细信息    查看全文

• 作者：Antti Valmari (1)
  
  1. Department of Mathematics ; Tampere University of Technology ; Tampere ; Finland
  
• 关键词：68Q85
• 刊名：Acta Informatica
• 出版年：2015
• 出版时间：April 2015
• 年：2015
• 卷：52
• 期：2-3
• 页码：207-234
• 全文大小：558 KB
• 参考文献：1. Aceto, L, Fokkink, WJ, Verhoef, C Structural operational semantics. In: Bergstra, JA, Ponse, A, Smolka, SA eds. (2001) Handbook of Process Algebra, Chapter 3. Elsevier, Amsterdam, pp. 197-292 CrossRef
  2. Arnold, A (1994) Finite Transition Systems. Prentice-Hall, Englewood Cliffs
  3. Austry, D, Boudol, G (1984) Alg猫bre de Processus et Synchronisation. Theoret. Comput. Sci. 30: pp. 91-131 CrossRef
  4. Bloom, B (1995) Structural operational semantics for weak bisimulations. Theoret. Comput. Sci. 146: pp. 25-68 CrossRef
  5. Bolognesi, T, Brinksma, E (1987) Introduction to the ISO Specification Language LOTOS. Comput. Netw. ISDN Syst. 14: pp. 25-59 CrossRef
  6. Boudol, G Notes on algebraic calculi of processes. In: Apt, K eds. (1985) Logics and Models of Concurrent Systems, NATO ASI Series F13. Springer, Berlin, pp. 261-303 CrossRef
  7. Simone, R (1985) Higher-level synchronising devices in Meije-SCCS. Theoret. Comput. Sci. 37: pp. 245-267 CrossRef
  8. Gibson-Robinson, T Efficient simulation of CSP-like languages. In: Welch, PH, Barnes, FRM, Broenink, JF, Chalmers, K, Pedersen, JB, Sampson, AT eds. (2013) Communicating Process Architectures 2013. Open Channel Publishing Ltd., Bicester, pp. 185-204
  9. Gorla, D (2010) Towards a unified approach to encodability and separation results for process calculi. Inf. Comput. 208: pp. 1031-1053 CrossRef
  10. Kaivola, R., Valmari, A.: The weakest compositional semantic equivalence preserving nexttime-less linear temporal logic. In: Cleaveland, R. (ed.) CONCUR 鈥?2, Third International Conference on Concurrency Theory, Lecture Notes in Computer Science, vol. 630, pp. 207鈥?21 (1992)
  11. Karsisto, K.: A new parallel composition operator for verification tools. Dr.Tech. Thesis, Tampere University of Technology Publications 420, Tampere, Finland (2003)
  12. Manna, Z, Pnueli, A (1992) The Temporal Logic of Reactive and Concurrent Systems, Volume I: Specification. Springer, Berlin CrossRef
  13. Milner, R (1989) Communication and Concurrency. Prentice-Hall, Englewood Cliffs
  14. Rensink, A, Vogler, W (2007) Fair testing. Inf. Comput. 205: pp. 125-198 CrossRef
  15. Roscoe, AW (2010) Understanding Concurrent Systems. Springer, Heidelberg CrossRef
  16. Valmari, A.: Failure-based equivalences are faster than many believe. In: Desel, J. (ed.) Structures in Concurrency Theory 1995, Springer-Verlag Workshops in Computing Series, pp. 326鈥?40 (1995)
  17. Valmari, A (1995) The weakest deadlock-preserving congruence. Inf. Process. Lett. 53: pp. 341-346 CrossRef
  18. Valmari, A.: Stubborn set methods for process algebras. In: Peled, D.A., Pratt, V.R., Holzmann, G.J. (eds.) Partial Order Methods in Verification: DIMACS Workshop, DIMACS Series in Discrete Mathematics and Theoretical Computer Science, vol. 29, pp. 213鈥?31. American Mathematical Society (1997)
  19. Valmari, A.: A Chaos-free failures divergences semantics with applications to verification. In: Davies, J., Roscoe, B., Woodcock, J. (eds.) Millennial Perspectives in Computer Science, Proceedings of the 1999 Oxford-Microsoft Symposium in Honour of sir Tony Hoare, Palgrave, pp. 365鈥?82 (2000)
  20. Valmari, A (2013) All linear-time congruences for familiar operators. Log. Methods Comput. Sci. 9: pp. 1-34
  21. Valmari, A, Tienari, M (1995) Compositional failure-based semantic models for basic LOTOS. Formal Aspects Comput. 7: pp. 440-468 CrossRef
  22. Glabbeek, R (2011) On cool congruence formats for weak bisimulations. Theoret. Comput. Sci. 412: pp. 3283-3302 CrossRef
  23. van Glabbeek, R.: Musings on encodings and expressiveness. In: Luttik, B., Reniers, M.A. (eds.) Proceedings of Combined 19th International Workshop on Expressiveness in Concurrency and 9th Workshop on Structured Operational Semantics, Electronic Proceedings in Theoretical Computer Science, vol. 89, pp. 81鈥?8 (2012)
  24. van Glabbeek, R., Weijland, W.: Branching time and abstraction in bisimulation semantics (Extended Abstract). In: Ritter, G. (ed.) Proceedings of IFIP International Conference on Information Processing 鈥?9, pp. 613鈥?18. North-Holland (1989)
  
• 刊物类别：Computer Science
• 刊物主题：Logics and Meanings of Programs
  Computer Systems Organization and Communication Networks
  Software Engineering, Programming and Operating Systems
  Data Structures, Cryptology and Information Theory
  Theory of Computation
  Information Systems and Communication Service
  
• 出版者：Springer Berlin / Heidelberg
• ISSN：1432-0525

文摘

An LTS operator can be constructed from a set of LTS operators up to an equivalence if and only if there is an LTS expression that only contains operators from the set and whose result is equivalent to the result of the operator. In this publication this idea is made precise in the context where each LTS has an alphabet of its own and the operators may depend on the alphabets. Then the extent to which LTS operators are constructible is studied. Most, if not all, established LTS operators have the property that each trace of the result arises from the execution of no more than one trace of each of its argument LTSs, and similarly for infinite traces. All LTS operators that have this property and satisfy some other rather weak regularity properties can be constructed from parallel composition and hiding up to the equivalence that compares the alphabets, traces, and infinite traces of the LTSs. Furthermore, a collection of other miscellaneous constructibility and unconstructibility results is presented.