Title :
BCTL: a branching clock temporal logic
Author :
Liu, Chuchang ; Orgun, Mehmet A.
Author_Institution :
Dept. of Comput., Macquarie Univ., NSW, Australia
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: ∀□, ∀?, ∃□ and ∃?. This logic can be used to describe nondeterministic programs and concurrent systems
Keywords :
logic programming; logic programming languages; programming theory; temporal logic; trees (mathematics); BCTL; Chronolog programs; branching clock temporal logic; branching time; concurrent systems; logic programming; next-bounded symbol; nondeterministic programs; temporal operators; Clocks; Computer languages; Linearity; Logic programming; Timing;
Conference_Titel :
Temporal Representation and Reasoning, 1997. (TIME '97), Proceedings., Fourth International Workshop on
Conference_Location :
Dayton Beach, FL
Print_ISBN :
0-8186-7937-9
DOI :
10.1109/TIME.1997.600795
