Model checking properties on reduced trace systems (Q1736621)
From MaRDI portal
scientific article
Language | Label | Description | Also known as |
---|---|---|---|
English | Model checking properties on reduced trace systems |
scientific article |
Statements
Model checking properties on reduced trace systems (English)
0 references
26 March 2019
0 references
Summary: Temporal logic has become a well-established method for specifying the behavior of distributed systems. In this paper, we interpret a temporal logic over a partial order model that is a trace system. The satisfaction of the formulae is directly defined on traces on the basis of rewriting rules; so, the graph representation of the system can be completely avoided; moreover, a method is presented that keeps the trace system finite, also in the presence of infinite computations. To further reduce the complexity of model checking temporal logic formulae, an abstraction technique is applied to trace systems.
0 references
trace systems
0 references
model checking
0 references
linear temporal logic
0 references
branching-time temporal logic
0 references
state explosion
0 references
0 references
0 references
0 references