Online Version - Last Updated - 20 Jan 2012 |
 |
| Home |
| |
| Procedures and Resources for Authors |
|
| Information and Resources for Volume Editors |
| |
| Orders and Subscriptions |
| |
| Published Articles |
|
| Upcoming Volumes |
| |
| Contact Us |
| |
| Useful External Links |
| |
| CRPIT Site Search |
The Relative Completeness of a Version of CTL*
Machi, H., Tomita, K. and Hosono, C.
We show the relative completeness of a version of CTL* over possibly infinite states. It is based on a fair discrete system, which is with strong and weak fairness. Validity of a CTL* formula is reduced to the validity of an assertion by eliminating the temporal operators and path quantifiers inductively. The idea is to represent the predicate describing that 'a fair path begins with the current state' in the underlying assertion language using fixpoint operators.
Cite as: Machi, H., Tomita, K. and Hosono, C. (2005). The Relative Completeness of a Version of CTL*. In Proc. Eleventh Computing: The Australasian Theory Symposium (CATS2005), Newcastle, Australia. CRPIT, 41. Atkinson, M. and Dehne, F., Eds. ACS. 81-85.
(from crpit.com)
(local if available)
