Edinburgh Research Archive logo

Edinburgh Research Archive

University of Edinburgh homecrest
View Item 
  •   ERA Home
  • Informatics, School of
  • Informatics thesis and dissertation collection
  • View Item
  •   ERA Home
  • Informatics, School of
  • Informatics thesis and dissertation collection
  • View Item
  • Login
JavaScript is disabled for your browser. Some features of this site may not work without it.

The Algebra of Finite State Processes

View/Open
ECS-LFCS-95-328.dvi (356.0Kb)
ECS-LFCS-95-328.ps (611.0Kb)
Date
12/1995
Author
Sewell, Peter M
Metadata
Show full item record
Abstract
This thesis is concerned with the algebraic theory of finite state processes. The processes we focus on are those given by a signature with prefix, summation and recursion, considered modulo strong bisimulation. We investigate their equational and implicational theories. We first consider the existence of finite equational axiomatisations. In order to express an interesting class of equational axioms we embed the processes into a simply typed lambda calculus, allowing equation schemes with metasubstitutions to be expressed by pure equations. Two equivalences over the lambda terms are defined, an extensional equality and a higher order bisimulation. Under a restriction to first order variables these are shown to coincide and an examination of the coincidence shows that no finite equational axiomatisation of strong bisimulation can exist. We then encode the processes of Basic Process Algebra with iteration and zero (BPAdelta*) into this lambda calculus and show that it too is not finitely equationally axiomatisable, in sharp contrast to the extant positive result for the fragment without zero. For the implicational theory, we show the existence of finite computable complete sets of unifiers for finite sets of equations between processes (with zero order variables). It follows that the soundness of sequents over these is decidable. Some applications to the theories of higher order process calculi and non-well-founded sets are made explicit. ECS-LFCS-95-328, October 1995.
URI
http://hdl.handle.net/1842/400
Collections
  • Informatics thesis and dissertation collection

Library & University Collections HomeUniversity of Edinburgh Information Services Home
Privacy & Cookies | Takedown Policy | Accessibility | Contact
Privacy & Cookies
Takedown Policy
Accessibility
Contact
feed RSS Feeds

RSS Feed not available for this page

 

 

All of ERACommunities & CollectionsBy Issue DateAuthorsTitlesSubjectsPublication TypeSponsorSupervisorsThis CollectionBy Issue DateAuthorsTitlesSubjectsPublication TypeSponsorSupervisors
LoginRegister

Library & University Collections HomeUniversity of Edinburgh Information Services Home
Privacy & Cookies | Takedown Policy | Accessibility | Contact
Privacy & Cookies
Takedown Policy
Accessibility
Contact
feed RSS Feeds

RSS Feed not available for this page