The application of a resource logic to the non- temporal

Hayman, Jonathan

HP Development Company

关键词: business process analysis;    bunched implications;    concurrency;    demos;   

RP-ID  :  HPL-2003-194

学科分类：计算机科学（综合）

美国|英语

来源: HP Labs

【 摘 要 】

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