Expressiveness for Highly Nested Expressions in Linear Temporal Logic
In the case where one only uses the modalities always, sometime and next it is shown that nesting modalities do not constrain a model in the limit any more than a non-nested formula. It is also proved that when the until modality operator is included then nesting modalities does constrain the limit...
| Main Author: | |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
1994.
|
| Subjects: | |
| Online Access: | Get fulltext |