BCTL

A branching clock temporal logic

Chuchang Liu*, Mehmet A. Orgun

*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceedingConference proceeding contribution

1 Citation (Scopus)

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 languageEnglish
Title of host publicationProceedings of the International Workshop on Temporal Representation and Reasoning
Place of PublicationLos Alamitos, CA
PublisherInstitute of Electrical and Electronics Engineers (IEEE)
Pages140-147
Number of pages8
Publication statusPublished - 1997
EventProceedings of the 1997 4th International Workshop on Temporal Representation and Reasoning - Daytona Beach, FL, USA
Duration: 10 May 199711 May 1997

Other

OtherProceedings of the 1997 4th International Workshop on Temporal Representation and Reasoning
CityDaytona Beach, FL, USA
Period10/05/9711/05/97

Fingerprint Dive into the research topics of 'BCTL: A branching clock temporal logic'. Together they form a unique fingerprint.

Cite this