Skip to content Skip to navigation
University of Warwick
  • Study
  • |
  • Research
  • |
  • Business
  • |
  • Alumni
  • |
  • News
  • |
  • About

University of Warwick
Publications service & WRAP

Highlight your research

  • WRAP
    • Home
    • Search WRAP
    • Browse by Warwick Author
    • Browse WRAP by Year
    • Browse WRAP by Subject
    • Browse WRAP by Department
    • Browse WRAP by Funder
    • Browse Theses by Department
  • Publications Service
    • Home
    • Search Publications Service
    • Browse by Warwick Author
    • Browse Publications service by Year
    • Browse Publications service by Subject
    • Browse Publications service by Department
    • Browse Publications service by Funder
  • Statistics
  • Help & Advice
University of Warwick

The Library

  • Login

Adding conflict and confusion to CSP

Tools
- Tools
+ Tools

UNSPECIFIED (2005) Adding conflict and confusion to CSP. In: 13th International Symposium of Formal Methods Europe, JUL 18-22, 2005, Tyne, ENGLAND.

Full text not available from this repository.

Abstract

In the development of concurrent systems two differing approaches have arisen: those with truly concurrent semantics and those with interleaving semantics. The difference between these two approaches is that in the coarser interleaving interpretation parallelism can be captured in terms of non-determinism whereas in the finer truly concurrent interpretation it cannot. Thus processes a vertical bar vertical bar b and a.b + b.a are identified within the interleaving approach but distinguished within the truly concurrent approach. In this paper we explore the truly concurrent notions of conflict, whereby transitions can occur individually but not together from a given state, and confusion, whereby the conflict set of a given transition is altered by the occurence of another transition with which it does not interfere. Having provided a translation from Petri nets, a truly concurrent formalism, to CSP, an interleaving formalism, we demonstate how the CSP model-checker FDR can be used to detect the presence of both conflict and confusion in Petri nets. This work is of interest for two reasons. Firstly, from a practical point of view: to the author's knowledge, no existing tool for modelling Petri nets can perform these checks and we address that issue. Secondly, and perhaps more significantly, we bridge the gap between truly concurrent and interleaving formalisms, demonstrating that true concurrency can be captured in what is typically considered to be an interleaving language.

Item Type: Conference Item (UNSPECIFIED)
Subjects: Q Science > QA Mathematics > QA76 Electronic computers. Computer science. Computer software
Series Name: LECTURE NOTES IN COMPUTER SCIENCE
Journal or Publication Title: FM 2005: FORMAL METHODS, PROCEEDINGS
Publisher: SPRINGER-VERLAG BERLIN
ISBN: 3-540-27882-6
ISSN: 0302-9743
Editor: Fitzgerald, J and Hayes, IJ and Tarlecki, A
Date: 2005
Volume: 3582
Number of Pages: 16
Page Range: pp. 205-220
Publication Status: Published
Title of Event: 13th International Symposium of Formal Methods Europe
Location of Event: Tyne, ENGLAND
Date(s) of Event: JUL 18-22, 2005
URI: http://wrap.warwick.ac.uk/id/eprint/6694

Data sourced from Thomson Reuters' Web of Knowledge

Request changes to a record

Actions (login required)

View Item View Item
twitter

Email us: publications@warwick.ac.uk
Contact Details
About Us