{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T04:42:41Z","timestamp":1750308161171,"version":"3.41.0"},"reference-count":12,"publisher":"Association for Computing Machinery (ACM)","issue":"3","license":[{"start":{"date-parts":[[2004,7,1]],"date-time":"2004-07-01T00:00:00Z","timestamp":1088640000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Comput. Logic"],"published-print":{"date-parts":[[2004,7]]},"abstract":"<jats:p>Value passing process algebras with infinite data domains need to be equipped with symbolic semantic models in order for their analysis to be possible. This means that appropriate symbolic models and the related verification algorithms must be developed, together with suitable semantic rules mapping the value passing process descriptions to such symbolic models. In this article, we first introduce the model of the symbolic transition graphs with lookahead assignment (STGLAs), a variant of the symbolic transition graphs with assignment (STGAs) of Lin that can undergo to the strong, weak and observational bisimulation equivalence checking algorithms of Li and Chen. We then define a set of symbolic semantic rules that map a useful fragment of value passing CCS to finite STGLAs without making any assumption about the variable names. We demonstrate that the symbolic semantic rules are correct with respect to both the usual concrete semantic rules and the novel issue of the assignment application order. Finally, we prove that, for the considered fragment of value passing CCS, the STGLAs produced by the symbolic semantic rules are optimal with respect to a certain compactness criterion, thus improving on the symbolic models and the semantic rules previously proposed in the literature.<\/jats:p>","DOI":"10.1145\/1013560.1013563","type":"journal-article","created":{"date-parts":[[2004,10,7]],"date-time":"2004-10-07T17:38:56Z","timestamp":1097170736000},"page":"436-469","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":2,"title":["Symbolic semantic rules for producing compact STGLAs from value passing process descriptions"],"prefix":"10.1145","volume":"5","author":[{"given":"Marco","family":"Bernardo","sequence":"first","affiliation":[{"name":"University of Urbino---Italy"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2004,7]]},"reference":[{"doi-asserted-by":"publisher","key":"e_1_2_1_1_1","DOI":"10.1145\/379525.379526"},{"doi-asserted-by":"publisher","key":"e_1_2_1_2_1","DOI":"10.1145\/362946.362970"},{"key":"e_1_2_1_3_1","volume-title":"Proceedings of the 5th International Workshop on Process Algebra and Performance Modelling (PAPM '97)","author":"Bernardo M.","year":"1997","unstructured":"Bernardo , M. 1997 . Enriching empa with value passing: A symbolic approach based on lookahead . In Proceedings of the 5th International Workshop on Process Algebra and Performance Modelling (PAPM '97) . 35--49.]] Bernardo, M. 1997. Enriching empa with value passing: A symbolic approach based on lookahead. In Proceedings of the 5th International Workshop on Process Algebra and Performance Modelling (PAPM '97). 35--49.]]"},{"key":"e_1_2_1_4_1","volume-title":"Proceedigns of the 9th International Symposium on Modeling, Analysis and Simulation of Computer and Telecommunication Systems (MASCOTS","author":"Bernardo M.","year":"2001","unstructured":"Bernardo , M. 2001 . A simulation analysis of dynamic server selection algorithms for replicated Web services . In Proceedigns of the 9th International Symposium on Modeling, Analysis and Simulation of Computer and Telecommunication Systems (MASCOTS 2001). IEEE Computer Science Press, Los Alamitos, CA, 371--378.]] Bernardo, M. 2001. A simulation analysis of dynamic server selection algorithms for replicated Web services. In Proceedigns of the 9th International Symposium on Modeling, Analysis and Simulation of Computer and Telecommunication Systems (MASCOTS 2001). IEEE Computer Science Press, Los Alamitos, CA, 371--378.]]"},{"unstructured":"Bernardo M. 2002. TwoTowers 2.0 User Manual. Available online at: www.sti.uniurb.it\/bernardo\/twotowers\/.]]  Bernardo M. 2002. TwoTowers 2.0 User Manual. Available online at: www.sti.uniurb.it\/bernardo\/twotowers\/.]]","key":"e_1_2_1_5_1"},{"doi-asserted-by":"crossref","unstructured":"Boudol G. and Castellani I. 1988. A non-interleaving semantics for ccs based on proved transitions. Fund. Informaticae XI 433--452.]]  Boudol G. and Castellani I. 1988. A non-interleaving semantics for ccs based on proved transitions. Fund. Informaticae XI 433--452.]]","key":"e_1_2_1_6_1","DOI":"10.3233\/FI-1988-11406"},{"doi-asserted-by":"publisher","key":"e_1_2_1_7_1","DOI":"10.1145\/151646.151648"},{"doi-asserted-by":"publisher","key":"e_1_2_1_8_1","DOI":"10.1016\/0304-3975(94)00172-F"},{"key":"e_1_2_1_9_1","volume-title":"Proceedigns of the 5th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS","volume":"1579","author":"Li Z.","year":"1999","unstructured":"Li , Z. and Chen , H . 1999. Computing strong\/weak bisimulation equivalences and observation congruence for value-passing processes . In Proceedigns of the 5th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 1999 ). Lecture Notes in Computer Science , vol. 1579 . Springer, Berlin, Germany, 300--314.]] Li, Z. and Chen, H. 1999. Computing strong\/weak bisimulation equivalences and observation congruence for value-passing processes. In Proceedigns of the 5th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 1999). Lecture Notes in Computer Science, vol. 1579. Springer, Berlin, Germany, 300--314.]]"},{"key":"e_1_2_1_10_1","volume-title":"Proceedigns of the 7th International Conference on Concurrency Theory (CONCUR","volume":"1119","author":"Lin H.","year":"1996","unstructured":"Lin , H. 1996 . Symbolic transition graph with assignment . In Proceedigns of the 7th International Conference on Concurrency Theory (CONCUR 1996). Lecture Notes in Computer Science , vol. 1119 . Springer, Berlin, Germany, 50--65.]] Lin, H. 1996. Symbolic transition graph with assignment. In Proceedigns of the 7th International Conference on Concurrency Theory (CONCUR 1996). Lecture Notes in Computer Science, vol. 1119. Springer, Berlin, Germany, 50--65.]]"},{"doi-asserted-by":"crossref","unstructured":"Lin H. 1998. On-the-fly instantiation of value-passing processes. In Proceedigns of the IFIP Joint International Conference on Formal Description Techniques for Distributed Systems and Communication Protocols and Protocol Specification Testing and Verification (FORTE\/PSTV 1998). Kluwer Amsterdam The Netherlands 215--230.]]   Lin H. 1998. On-the-fly instantiation of value-passing processes. In Proceedigns of the IFIP Joint International Conference on Formal Description Techniques for Distributed Systems and Communication Protocols and Protocol Specification Testing and Verification (FORTE\/PSTV 1998). Kluwer Amsterdam The Netherlands 215--230.]]","key":"e_1_2_1_11_1","DOI":"10.1007\/978-0-387-35394-4_14"},{"volume-title":"Communication and Concurrency","author":"Milner R.","unstructured":"Milner , R. 1989. Communication and Concurrency . Prentice Hall , Englewood Cliffs, NJ .]] Milner, R. 1989. Communication and Concurrency. Prentice Hall, Englewood Cliffs, NJ.]]","key":"e_1_2_1_12_1"}],"container-title":["ACM Transactions on Computational Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1013560.1013563","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1013560.1013563","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T16:19:03Z","timestamp":1750263543000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1013560.1013563"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004,7]]},"references-count":12,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2004,7]]}},"alternative-id":["10.1145\/1013560.1013563"],"URL":"https:\/\/doi.org\/10.1145\/1013560.1013563","relation":{},"ISSN":["1529-3785","1557-945X"],"issn-type":[{"type":"print","value":"1529-3785"},{"type":"electronic","value":"1557-945X"}],"subject":[],"published":{"date-parts":[[2004,7]]},"assertion":[{"value":"2004-07-01","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}