Projects per year
Abstract
Unique Fixpoint Induction (UFI) is the chief inference rule to prove the equivalence of recursive processes in the Calculus of Communicating Systems (CCS) (Milner 1989). It plays a major role in the equational approach to verification. Equational verification is of special interest as it offers theoretical advantages in the analysis of systems that communicate values, have infinite state space or show parameterised behaviour. We call these kinds of systems VIPSs. VIPSs is the acronym of Valuepassing, InfiniteState and Parameterised Systems. Automating the application of UFI in the context of VIPSs has been neglected. This is both because many VIPSs are given in terms of recursive function symbols, making it necessary to carefully apply induction rules other than UFI, and because proving that one VIPS process constitutes a fixpoint of another involves computing a process substitution, mapping states of one process to states of the other, that often is not obvious. Hence, VIPS verification is usually turned into equation solving (Lin 1995a). Existing tools for this proof task, such as VPAM (Lin 1993), are highly interactive. We introduce a method that automates the use of UFI. The method uses middleout reasoning (Bundy et al. 1990a) and, so, is able to apply the rule even without elaborating the details of the application. The method introduces metavariables to represent those bits of the processes’ state space that, at application time, were not known, hence, changing from equation verification to equation solving. Adding this method to the equation plan developed by Monroy et al. (Autom Softw Eng 7(3):263–304, 2000a), we have implemented an automatic verification planner. This planner increases the number of verification problems that can be dealt with fully automatically, thus improving upon the current degree of automation in the field.
Original language  English 

Pages (fromto)  5380 
Number of pages  28 
Journal  Journal of Automated Reasoning 
Volume  43 
Issue number  1 
DOIs  
Publication status  Published  Jun 2009 
Keywords
 Unique fixpoint induction
 Equational verification
 Calculus of communicating systems
Fingerprint Dive into the research topics of 'On Process Equivalence = Equation Solving in CCS'. Together they form a unique fingerprint.
Projects
 1 Finished

Integration and Interaction of multiple mathematical reasoning processes
Bundy, A., Colton, S., Aspinall, D., Dennis, L., Fleuriot, J., Georgieva, L., Ireland, A., Jackson, P. & Smaill, A.
1/04/07 → 31/03/11
Project: Research