| EPSRC Reference: |
GR/T19407/01 |
| Title: |
CASINO: CAusal SemantIcs of Nets with inhibitOr arcs |
| Principal Investigator: |
Koutny, Professor M |
| Other Investigators: |
|
| Researcher Co-Investigators: |
|
| Project Partners: |
|
| Department: |
Computing Sciences |
| Organisation: |
Newcastle University |
| Scheme: |
Standard Research (Pre-FEC) |
| Starts: |
25 November 2004 |
Ends: |
24 November 2007 |
Value (£): |
9,055
|
| EPSRC Research Topic Classifications: |
| Fundamentals of Computing |
|
|
| EPSRC Industrial Sector Classifications: |
| No relevance to Underpinning Sectors |
|
|
| Related Grants: |
|
| Panel History: |
|
|
Summary on Grant Application Form |
|
The overall aim of the proposed visits is to complete the development of the fundamental part of the causality semantics for nets with inhibitor arcs which are used in the modelling and analysis of complex concurrent systems, and to investigate whether such a semantics can be used to develop efficient verification techniques. To achieve the first objective we will proceed by adopting (and, if necessary, modifying) those ideas which had proved effective for our prior work on finite causal nets generated by inhibitor nets. We expect that the existing framework is sufficiently developed to allow a relatively straightforward definition of the operational way in which such causal nets are generated. This, however, needs to be complemented by a suitable axiomatic definition which is much harder to formulate and then prove equivalent with the operational one. The second objective brings into the framework the issue of conflict in the behaviour specified by inhibitor nets. We plan to conduct a comprehensive study of the relationship between (weak and strong) causality and action conflict in the context of inhibitor nets. The third objective is to investigate the ways in which a (typically infinite) unfolding could be truncated to a finite representative (its prefix) which would still have full information about the state space of the original inhibitor net, and we plan to re-evaluate the thinking behind the prefix-based approach to the verification of the standard Petri nets.
|
|
Key Findings |
|
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk
|
|
Potential use in non-academic contexts |
|
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk
|
|
Impacts |
|
| Description |
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk |
| Summary |
|
| Date Materialised |
|
|
|
|
Sectors submitted by the Researcher |
|
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk
|
| Project URL: |
|
| Further Information: |
|
| Organisation Website: |
http://www.ncl.ac.uk |