Loading...
Please wait, while we are loading the content...
Similar Documents
Petri Nets, Traces, and Local Model Checking (1995)
| Content Provider | CiteSeerX |
|---|---|
| Author | Cheng, Allan |
| Description | Proceedings of the 4th International Conference on Algebraic Methodology and Software Technology, Lecture Notes in Computer Science 936, SpringerVerlag |
| Abstract | It has been observed that the behavioural view of concurrent systems that all possible sequences of actions are relevant is too generous; Not all sequences should be considered as likely behaviours. By taking progress fairness assumptions into account one obtains a more realistic behavioural view of the systems. In this paper we consider the problem of performing model checking relative to this behavioural view. We present a CTL-like logic which is interpreted over the model of concurrent systems labeled 1-safe nets. It turns out that Mazurkiewicz trace theory provides a useful setting in which the progress fairness assumptions can be formalized in a natural way. We provide the first, to our knowledge, set of sound and complete tableau rules for a CTL-like logic interpreted under progress fairness assumptions. keywords: fair progress, labeled 1-safe nets, local model checking, maximal traces, partial orders, inevitability 1 Introduction Recently attention has focused on behavioural v... |
| File Format | |
| Publisher Date | 1995-01-01 |
| Access Restriction | Open |
| Subject Keyword | 1-safe Net Partial Order Likely Behaviour Possible Sequence Useful Setting Natural Way Mazurkiewicz Trace Theory Local Model Checking Introduction Recently Attention Complete Tableau Rule Ctl-like Logic Maximal Trace Fair Progress Behavioural View Concurrent System Realistic Behavioural View Progress Fairness Assumption Petri Net |
| Content Type | Text |
| Resource Type | Proceeding Conference Proceedings Article |
