It is well known that through code instrumentation, a distributed system's finite execution can generate a finite trace as a partially ordered set of events. We motivate the need to use LTL model-checking on sequences and not on traces as defined by Diekert and Gastin, to validate distributed control systems executions, abstracted by such traces, and present an efficient symbolic algorithm to do the job. It uses the standard method proposed by Vardi and Wolper, which from the LTL formula, builds a monitor that accepts all the bad sequences. We show that, given a monitor and a trace, the problem to check that both the monitor and the trace have a common sequence is NP-complete in the number of concurrent processes. Our method explores the possible configurations symbolically, since it handles sets of configurations. Moreover, it uses techniques similar to the partial order reduction, to avoid exploring as many execution interleavings as possible. It works very well in practice, compared to the standard exploration method, with or without partial order reduction (which, in practice, does not work well here). © Springer-Verlag Berlin Heidelberg 2006.
CITATION STYLE
Genon, A., Massart, T., & Meuter, C. (2006). Monitoring distributed controllers: When an efficient LTL algorithm on sequences is needed to model-check traces. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 4085 LNCS, pp. 557–572). Springer Verlag. https://doi.org/10.1007/11813040_37
Mendeley helps you to discover research relevant for your work.