DocumentCode
3129425
Title
BCTL: a branching clock temporal logic
Author
Liu, Chuchang ; Orgun, Mehmet A.
Author_Institution
Dept. of Comput., Macquarie Univ., NSW, Australia
fYear
1997
fDate
10-11 May 1997
Firstpage
140
Lastpage
147
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;
fLanguage
English
Publisher
ieee
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
Type
conf
DOI
10.1109/TIME.1997.600795
Filename
600795
Link To Document