{"id":{"repo_id":"uiuc","oai_identifier":"oai:www.ideals.illinois.edu:2142/50630"},"canonical_url":"https://search.dev.ndltd.org/etd/uiuc/oai:www.ideals.illinois.edu:2142/50630","repository":{"repo_id":"uiuc","name":"University of Illinois - Urbana-Champaign","base_url":"https://www.ideals.illinois.edu/oai-pmh"},"display":{"title":"Symbolic semantics for CSP","abstract":"Communicating Sequential Processes (CSP) is a well-known formal language for describing concurrent systems, for which a transition semantics has been given by Brookes, Hoare and Roscoe. In this thesis, we present a generalized transition semantics of CSP, which we call HCSP, that merges the original transition system with ideas from Floyd-Hoare logic and symbolic computation. This generalized semantics is shown to be sound and complete with respect to the original trace semantics. Traces in our system are symbolic representations of trace families given in the original semantics. This more compact representation allows us to expand the original CSP systems to effectively and efficiently analyze some CSP programs that are difficult or impossible for other CSP systems to analyze. In particular, our system can handle certain classes of non-deterministic choices as a single transition, while the original semantics would treat each choice separately, possibly leading to large or unbounded case analyses. All the work described in this thesis, carried out in the theorem prover Isabelle, provides us with a framework for automated and interactive analyses of CSP processes. It also gives us the ability to extract Ocaml code for an HCSP-based simulator directly from Isabelle.","abstract_html":"Communicating Sequential Processes (CSP) is a well-known formal language for describing concurrent systems, for which a transition semantics has been given by Brookes, Hoare and Roscoe. In this thesis, we present a generalized transition semantics of CSP, which we call HCSP, that merges the original transition system with ideas from Floyd-Hoare logic and symbolic computation. This generalized semantics is shown to be sound and complete with respect to the original trace semantics. Traces in our system are symbolic representations of trace families given in the original semantics. This more compact representation allows us to expand the original CSP systems to effectively and efficiently analyze some CSP programs that are difficult or impossible for other CSP systems to analyze. In particular, our system can handle certain classes of non-deterministic choices as a single transition, while the original semantics would treat each choice separately, possibly leading to large or unbounded case analyses. All the work described in this thesis, carried out in the theorem prover Isabelle, provides us with a framework for automated and interactive analyses of CSP processes. It also gives us the ability to extract Ocaml code for an HCSP-based simulator directly from Isabelle.","abstract_has_math":false,"creators":["Li, Liyi"],"institution":"University of Illinois at Urbana-Champaign","degree_name":"M.S.","degree_level":"Thesis","degree_discipline":"Computer Science","degree_department":null,"school":null,"contributors":["Gunter, Elsa L."],"advisors":[],"committee_chairs":[],"committee_members":[],"year":2014,"date_issued":"2014-09-16T17:24:32Z","date_published":"2014-09-16T17:24:32Z","updated_at":"2026-07-22T22:25:40Z","subjects":["Communicating Sequential Processes (CSP)","Process Algebra","Symbolic Semantics","Theorem Proving","Simulator"],"languages":["en"],"rights":["2014 by Liyi Li. All rights reserved."],"rights_urls":[],"identifier_entries":[]},"links":{"outbound_url":"http://hdl.handle.net/2142/50630","outbound_label":"Handle","outbound_source":"dc:identifier"},"metadata_groups":[{"id":"people","label":"People","entries":[{"key":"dc:contributor","label":"Contributor","values":["Gunter, Elsa L."]},{"key":"dc:creator","label":"Author","values":["Li, Liyi"]}]},{"id":"academic_context","label":"Academic Context","entries":[{"key":"dc:date","label":"Dc Date","values":["2014-09-16T17:24:32Z","2014-08","2014-09-16"]},{"key":"dc:type","label":"Dc Type","values":["text"]},{"key":"thesis:degree_discipline","label":"Discipline","values":["Computer Science"]},{"key":"thesis:degree_level","label":"Degree Level","values":["Thesis"]},{"key":"thesis:degree_name","label":"Degree Name","values":["M.S."]},{"key":"thesis:institution_name","label":"Thesis Institution Name","values":["University of Illinois at Urbana-Champaign"]}]},{"id":"subjects_keywords","label":"Subjects and Keywords","entries":[{"key":"dc:subject","label":"Dc Subject","values":["Communicating Sequential Processes (CSP)","Process Algebra","Symbolic Semantics","Theorem Proving","Simulator"]}]},{"id":"language_rights","label":"Language and Rights","entries":[{"key":"dc:language","label":"Dc Language","values":["en"]},{"key":"dc:rights","label":"Dc Rights","values":["2014 by Liyi Li. All rights reserved."]}]},{"id":"identifiers","label":"Identifiers","entries":[{"key":"dc:identifier","label":"Identifier","values":["http://hdl.handle.net/2142/50630"]}]},{"id":"additional","label":"Additional Metadata","entries":[{"key":"dc:description","label":"Description","values":["Communicating Sequential Processes (CSP) is a well-known formal language for describing concurrent systems, for which a transition semantics has been given by Brookes, Hoare and Roscoe. In this thesis, we present a generalized transition semantics of CSP, which we call HCSP, that merges the original transition system with ideas from Floyd-Hoare logic and symbolic computation. This generalized semantics is shown to be sound and complete with respect to the original trace semantics. Traces in our system are symbolic representations of trace families given in the original semantics. This more compact representation allows us to expand the original CSP systems to effectively and efficiently analyze some CSP programs that are difficult or impossible for other CSP systems to analyze. In particular, our system can handle certain classes of non-deterministic choices as a single transition, while the original semantics would treat each choice separately, possibly leading to large or unbounded case analyses. All the work described in this thesis, carried out in the theorem prover Isabelle, provides us with a framework for automated and interactive analyses of CSP processes. It also gives us the ability to extract Ocaml code for an HCSP-based simulator directly from Isabelle.","Item withdrawn by Mark Zulauf (zulauf@illinois.edu) on 2014-07-18T22:05:12Z Item was in collections: University of Illinois Theses & Dissertations (ID: 1) No. of bitstreams: 1 master.pdf: 583053 bytes, checksum: f91c625780c5afcfe045fef424d968bf (MD5)","Made available in DSpace on 2014-09-16T17:24:32Z (GMT). No. of bitstreams: 2 Liyi_Li.pdf: 583053 bytes, checksum: f91c625780c5afcfe045fef424d968bf (MD5) license.txt: 4056 bytes, checksum: 4290336f53970621aaca43cd3b78ecbc (MD5)"]},{"key":"dc:title","label":"Title","values":["Symbolic semantics for CSP"]}]}],"canonical_facts":{"dc:contributor":["Gunter, Elsa L."],"dc:creator":["Li, Liyi"],"dc:date":["2014-09-16T17:24:32Z","2014-08","2014-09-16"],"dc:description":["Communicating Sequential Processes (CSP) is a well-known formal language for describing concurrent systems, for which a transition semantics has been given by Brookes, Hoare and Roscoe. In this thesis, we present a generalized transition semantics of CSP, which we call HCSP, that merges the original transition system with ideas from Floyd-Hoare logic and symbolic computation. This generalized semantics is shown to be sound and complete with respect to the original trace semantics. Traces in our system are symbolic representations of trace families given in the original semantics. This more compact representation allows us to expand the original CSP systems to effectively and efficiently analyze some CSP programs that are difficult or impossible for other CSP systems to analyze. In particular, our system can handle certain classes of non-deterministic choices as a single transition, while the original semantics would treat each choice separately, possibly leading to large or unbounded case analyses. All the work described in this thesis, carried out in the theorem prover Isabelle, provides us with a framework for automated and interactive analyses of CSP processes. It also gives us the ability to extract Ocaml code for an HCSP-based simulator directly from Isabelle.","Item withdrawn by Mark Zulauf (zulauf@illinois.edu) on 2014-07-18T22:05:12Z Item was in collections: University of Illinois Theses & Dissertations (ID: 1) No. of bitstreams: 1 master.pdf: 583053 bytes, checksum: f91c625780c5afcfe045fef424d968bf (MD5)","Made available in DSpace on 2014-09-16T17:24:32Z (GMT). No. of bitstreams: 2 Liyi_Li.pdf: 583053 bytes, checksum: f91c625780c5afcfe045fef424d968bf (MD5) license.txt: 4056 bytes, checksum: 4290336f53970621aaca43cd3b78ecbc (MD5)"],"dc:identifier":["http://hdl.handle.net/2142/50630"],"dc:language":["en"],"dc:rights":["2014 by Liyi Li. All rights reserved."],"dc:subject":["Communicating Sequential Processes (CSP)","Process Algebra","Symbolic Semantics","Theorem Proving","Simulator"],"dc:title":["Symbolic semantics for CSP"],"dc:type":["text"],"thesis:degree_discipline":["Computer Science"],"thesis:degree_level":["Thesis"],"thesis:degree_name":["M.S."],"thesis:institution_name":["University of Illinois at Urbana-Champaign"]},"updated_at":"2026-07-22T22:25:40Z"}