Model checking properties on reduced trace systems (Q1736621): Difference between revisions
From MaRDI portal
Changed an Item |
Set OpenAlex properties. |
||
(One intermediate revision by one other user not shown) | |||
Property / MaRDI profile type | |||
Property / MaRDI profile type: MaRDI publication profile / rank | |||
Normal rank | |||
Property / full work available at URL | |||
Property / full work available at URL: https://doi.org/10.3390/a7030339 / rank | |||
Normal rank | |||
Property / OpenAlex ID | |||
Property / OpenAlex ID: W2081369054 / rank | |||
Normal rank |
Revision as of 20:29, 19 March 2024
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