| |
Click here for full text:
The application of a resource logic to the non- temporal analysis of processes acting on resources
Hayman, Jonathan
HPL-2003-194
Keyword(s): business process analysis; bunched implications; concurrency; demos
Abstract: Please Note. This abstract contains mathematical formulae which cannot be represented here. Many systems exist that can be modelled as processes interacting through shared resources -people, factories and computer systems to name but a few. Building upon a logic capable of reasoning about static resource models, the Logic of Bunched Implications, we tentatively define the semantics of a logic capable of reasoning about dynamic resource models. The logic shall not consider the influence of timing on process interaction. We give a brief overview of other process logics- Hennessy-Milner logic, Computation Tree Logic and modal- - which indicate how we may automate the system. We illustrate how our dynamic resource logic may be applied to the analysis of Petri nets. In order to conduct an analysis of processes, we must have a formal representation for them: we choose Demos, and present its salient characteristics. We give a formal definition of its non-time semantics, and prove that this is, in some sense, correct. Following consideration of how we apply our process logic to Demos models, we propose a method for reducing the state-space of models generated by considering a (partially) synchronous execution. We show that such a system at least correctly detects deadlock.
92 Pages
Back to Index
|
printable version
