Jump to content United States-English
HP.com Home Products and Services Support and Drivers Solutions How to Buy
» Contact HP

hp.com home


Technical Reports


printable version
» 

HP Labs

» Research
» News and events
» Technical reports
» About HP Labs
» Careers @ HP Labs
» Worldwide sites
» Downloads
Content starts here

 
Click here for full text: PDF

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

»Technical Reports

» 2009
» 2008
» 2007
» 2006
» 2005
» 2004
» 2003
» 2002
» 2001
» 2000
» 1990 - 1999

Heritage Technical Reports

» Compaq & DEC Technical Reports
» Tandem Technical Reports
Privacy statement Using this site means you accept its terms Feedback to HP Labs
© 2009 Hewlett-Packard Development Company, L.P.