Paper Info
Title
A monotone framework for CCS
Abstract
The calculus of communicating systems, CCS, was introduced by Robin Milner as a calculus for modelling concurrent systems. Subsequently several techniques have been developed for analysing such models in order to get further insight into their dynamic behaviour. In this paper we present a static analysis for approximating the control structure embedded within the models. We formulate the analysis as an instance of a monotone framework and thus draw on techniques that often are associated with the efficient implementation of classical imperative programming languages. We show how to construct a finite automaton that faithfully captures the control structure of a CCS model. Each state in the automaton records a multiset of the enabled actions and appropriate transfer functions are developed for transforming one state into another. A classical worklist algorithm governs the overall construction of the automaton and its termination is ensured using techniques from abstract interpretation.
Year
DOI
Venue
2009
10.1016/j.cl.2008.07.001
Computer Languages, Systems & Structures
Keywords
Field
DocType
finite automaton,control structure,automaton record,abstract interpretation,classical worklist algorithm,appropriate transfer function,robin milner,ccs model,monotone framework,classical imperative programming language,static analysis,calculus of communicating systems,ccs,programming language,transfer function,process calculi
Programming language,Deterministic automaton,Abstract interpretation,Computer science,Automaton,Calculus of communicating systems,Imperative programming,Theoretical computer science,Finite-state machine,Process calculus,Probabilistic automaton
Journal
Volume
Issue
ISSN
35
4
Computer Languages, Systems & Structures
Citations 
PageRank 
References 
8
0.62
17
Authors
2
Name
Order
Citations
PageRank
Hanne Riis Nielson11719153.77
flemming nielson21769172.05