Baader, FranzBauer, AndreasLippmann, Marcel2015-12-109783642042218http://hdl.handle.net/1885/57053Formulae 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 thisKeywords: 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 checki200910.1007/978-3-642-04222-5_92016-02-24