Abstract
This paper presents a branching time temporal logic called BCTL. In this logic, branching time is represented by branching clocks, which can be specified as Chronolog programs. In BCTL, formulas are allowed to be defined on different branching clocks. Apart from the temporal operators first and next, BCTL contains a next-bounded symbol ! and four modalities: for all square open for every ◆, there exists square open and ∃◆. This logic can be used to describe nondeterministic programs and concurrent systems.
| Original language | English |
|---|---|
| Title of host publication | Proceedings of the International Workshop on Temporal Representation and Reasoning |
| Place of Publication | Los Alamitos, CA |
| Publisher | Institute of Electrical and Electronics Engineers (IEEE) |
| Pages | 140-147 |
| Number of pages | 8 |
| Publication status | Published - 1997 |
| Event | Proceedings of the 1997 4th International Workshop on Temporal Representation and Reasoning - Daytona Beach, FL, USA Duration: 10 May 1997 → 11 May 1997 |
Other
| Other | Proceedings of the 1997 4th International Workshop on Temporal Representation and Reasoning |
|---|---|
| City | Daytona Beach, FL, USA |
| Period | 10/05/97 → 11/05/97 |