Cultural advice

The Australian National University acknowledges, celebrates and pays our respects to the Ngunnawal and Ngambri people of the Canberra region and to all First Nations Australians on whose traditional lands we meet and work, and whose cultures are among the oldest continuing cultures in human history.

Aboriginal and Torres Strait Islander peoples are advised that ANU Library collections may include images, names, voices, and other representations of deceased persons.

Material in the collection may contain terms, language or views that reflect the period in which the item was created and may be considered inappropriate today.

Runtime verification using a temporal description logic

Date

Authors

Baader, Franz

Bauer, Andreas

Lippmann, Marcel

Publisher

Springer

Abstract

Formulae of linear temporal logic (LTL) can be used to specify (wanted or unwanted) properties of a dynamical system. In model checking, the system's behavior is described by a transition system, and one needs to check whether all possible traces of this

Keywords

Keywords: Actual system; Complete information; Description logic; Finite prefix; Linear temporal logic; Observed systems; Propositional variables; Run-time verification; Single state; Time points; Transition system; Data description; Dynamical systems; Model checki

URI

http://hdl.handle.net/1885/57053

Collections

ANU Research Publications

Type

Book Title

Frontiers of Combining Systems

DOI

10.1007/978-3-642-04222-5_9

Restricted until

2037-12-31

Downloads

File

Description

01_Baader_Runtime_verification_using_a_2009.pdf (77.3 KB)

02_Baader_Runtime_verification_using_a_2009.pdf (78.29 KB)

03_Baader_Runtime_verification_using_a_2009.pdf (239.98 KB)