Handling Conflicts in Depth-First Search for LTL Tableau to Debug Compliance Based Languages

Francois Hantry
(UCBLyon France)
Mohand-Said Hacid
(UCBLyon France)

Providing adequate tools to tackle the problem of inconsistent compliance rules is a critical research topic. This problem is of paramount importance to achieve automatic support for early declarative design and to support evolution of rules in contract-based or service-based systems. In this paper we investigate the problem of extracting temporal unsatisfiable cores in order to detect the inconsistent part of a specification. We extend conflict-driven SAT-solver to provide a new conflict-driven depth-first-search solver for temporal logic. We use this solver to compute LTL unsatisfiable cores without re-exploring the history of the solver.

In Ernesto Pimentel and Valentín Valero: Proceedings Fifth Workshop on Formal Languages and Analysis of Contract-Oriented Software (FLACOS 2011), Málaga, Spain, 22nd and 23rd September 2011, Electronic Proceedings in Theoretical Computer Science 68, pp. 39–53.
Published: 12th September 2011.

ArXived at: http://dx.doi.org/10.4204/EPTCS.68.5 bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org