Name
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 behaviour is described by a transition system, and one needs to check whether all possible traces of this transition system satisfy the formula. In runtime verification, one observes the actual system behaviour, which at any point in time yields a finite prefix of a trace. The task is then to check whether all continuations of this prefix to a trace satisfy (violate) the formula. More precisely, one wants to construct a monitor, i.e., a finite automaton that receives the finite prefix as input and then gives the right answer based on the state currently reached. |
Year | DOI | Venue |
|---|---|---|
2014 | 10.1016/j.jal.2014.09.001 | Journal of Applied Logic |
Keywords | Field | DocType |
Temporal description logics,Runtime verification,Monitoring | Computation tree logic,Transition system,Discrete mathematics,Model checking,Satisfiability,Algorithm,Linear temporal logic,Theoretical computer science,Runtime verification,Temporal logic,Propositional variable,Mathematics | Journal |
Volume | Issue | ISSN |
12 | 4 | 1570-8683 |
Citations | PageRank | References |
1 | 0.35 | 22 |
Authors | ||
2 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Franz Baader | 1 | 8123 | 646.64 |
| Marcel Lippmann | 2 | 112 | 6.98 |