Loading...
Please wait, while we are loading the content...
Similar Documents
A Resolution Method for CTL Branching-Time Temporal Logic (1997)
| Content Provider | CiteSeerX |
|---|---|
| Author | Bolotov, Alexander Fisher, Michael |
| Description | In this paper we extend our clausal resolution method for linear temporal logics to a branching-time framework. The branching-time temporal logics considered are Computation Tree Logic (CTL), often regarded as the simplest useful logic of this class, and Extended CTL (ECTL), which is CTL extended with fairness operators. The key elements of the resolution method, namely the normal form, the concept of step resolution and a novel temporal resolution rule, are introduced and justified with respect to both these logics. A completeness argument is provided, together with an example of the use of the temporal resolution method. Finally, we consider future work, in particular extension of the method yet further, to CTL , and implementation of the approach by utilising techniques developed for linear-time temporal resolution. |
| File Format | |
| Language | English |
| Publisher | IEEE Press |
| Publisher Date | 1997-01-01 |
| Publisher Institution | IN PROCEEDINGS OF THE FOURTH INTERNATIONAL WORKSHOP ON TEMPORAL REPRESENTATION AND REASONING (TIME |
| Access Restriction | Open |
| Subject Keyword | Fairness Operator Linear Temporal Logic Ctl Branching-time Temporal Logic Extended Ctl Branching-time Temporal Logic Key Element Useful Logic Novel Temporal Resolution Rule Normal Form Particular Extension Clausal Resolution Method Branching-time Framework Linear-time Temporal Resolution Step Resolution Completeness Argument Temporal Resolution Method Resolution Method Computation Tree Logic Future Work |
| Content Type | Text |
| Resource Type | Article |
