EquivalenceChecker For Timed CCS
 
 

İrem Aktuğ
Department of Computer Engineering,
Middle East Technical University

Supervisors: Halit Oğuztüzün, Serkan A.Karataş

Senior Design Project and Seminar, CENG490
Coordinators: Dr. Ferda N. Alpaslan, Dr.Volkan Atalay
Teaching Assistant: Gürkan Özhan, ÖzgurAlan
 
 
 

Date:    6th October 2000
 
 

Motivation and Purpose

    The subject of concurrency is being studied as a mathematical model. Equivalence in this sense is well-defined. But it is hard to cope with the increasing state space of the models manually. The area needs an efficient and user friendly tool to be able to continue research in an accurate manner.
 
 

Project Description

    Timed CCS(Calculus of Communicating Systems) deals with agents that do some actions and/or communicate with other agents with time constraints. In this model there can be various relations of equivalence between two agents. All of the relations are defined mathematically over the agents' state and action sets. Especially, observational equivalence is used very often. For example, an agent that is behaviourally equivalent to another can replace that one in a system.
    I will implement a tool to decide whether or not two agents are behaviourally equivelant.
 
 

Statement of the Work to be Performed

    An efficient algorithm(hopefully running in polynomial time) will be devised to decide equilvalence of two agents and implemented into a tool. The tool will give error messages, i.e. tell why the agents are not equivalent, so it will help the user reach his/her aim.
 
 

Current State of the Art in Turkey and in the World

    Believing that the common semantic framework of mathematical functions for sequential programming is not enough to explain concurrency,Robert Milner developed a semantic theory of processes called Calculus of Communicating Systems. The theory was published in 1980. It is based on a notion of bisimulation equivalence. Bisimulation semantics is an elegant mathmematical theory of processes. It provides simple and elegant proof techniques for showing that a process implementation meets its specifications.So it is actually very valuable for practical purposes as well as laying a theoretical basis for concurrent and communicating systems.
    Timed CCS is an extension of Milner's CCS. It was needed because of the time constraints that many real time systems have. Several Timed CCS's have been constructed. The one that I will use was offered by Liang Chen in his doctoral thesis in 1992.
    Currently the subject is studied in universities,and is mainly a theoretical subject. But since it can prove that a system meets its specifications, it is worth to use to verify for safety critical systems, like air-ground data link protocols.
 
 

Approach and Method to be Used

    I have done a survey in the literature and found some interesting papers that can be of help. An equivalence checking algorithm is suggested by one particular paper: CCS Expressions, Finite State Processes,and Three Problems of Equivalence. In this paper, Tarjan&Paige’s PartitionRefinement Algorithms are particularly referred to. So I will use these two papers. But the algorithm is for the original CCS, not for the timed one. So I plan to revise it to work for Timed CCS. And after I specify an efficient algorithm for the task, I will implement it into a tool that also produces useful error messages.
 
 

Major Milestones

     15 November - ProgressReport Deadline: I plan to have an algorithm
                     that solves the problem by this date. I hope to present the
                     algorithm in my report.
     15 December - FinalReport Deadline: I plan to have a tool that runs in
                     polynomial time by this date.
      2 January - Demonstration: I plan to present the tool with full user interfaceon
                     this date.
 

Coarse Project Plan and Schedule

        WP1: Devising an Algorithm

         task1:Understanding the suggested algorithm
         task2:Making the algorithm specific
        task3: Revising the algorithm to work for Timed CCS

       WP2:Implementation

         task1:Implementing the algorithm
         task2:Adding user interface
 
 
 

Resources

    Prolog programming language is needed to implement the tool.
 
 

Bibliography

    R. Milner, Turing Award Lecture, Elements of Interaction,Communications of ACM, Jan 1993
    R. Milner, Communication and Concurrency, Prentice-HallInternational, 1989
    L. Chen, Timed Processes: Models, Axioms, and Decidability,Ph.D. Thesis, University of Edinburgh, 1992
    C. Fencott, Formal Methods for Concurrency, ThomsonComputer Press, 1996
    R. Paige, R. E. Tarjan: Three Partition RefinementAlgorithms. Pp.973-989, SIAMJ on Computing 16(6), 1987
    P. C. Kanellakis, S. A. Smolka, CCS Expressions,Finite State Processes, and Three Problems of Equivalence,
    Information and Computation, 86(1):43-68, May 1990
    Lists of Computer Science Journals and other publications:
    http://elib.cs.sfu.ca/cs-journals/
    http://www.informatik.uni-trier.de/~ley/db/journals