Finite Models vs Tree Automata in Safety Verification

Lisitsa, Alexei

doi:10.4230/LIPIcs.RTA.2012.225

Document

Finite Models vs Tree Automata in Safety Verification

Author Alexei Lisitsa

Part of: Volume: 23rd International Conference on Rewriting Techniques and Applications (RTA'12) (RTA 2012)
Part of: Series: Leibniz International Proceedings in Informatics (LIPIcs)
Part of: Conference: International Conference on Rewriting Techniques and Applications (RTA)
License: Creative Commons Attribution-NonCommercial-NoDerivs 3.0 Unported license
Publication Date: 2012-05-29

PDF

File

PDF

LIPIcs.RTA.2012.225.pdf

Filesize: 400 kB
15 pages

Document Identifiers

DOI: 10.4230/LIPIcs.RTA.2012.225
URN: urn:nbn:de:0030-drops-34959

Subject Classification

Keywords

term-rewriting systems
safety verification
first-order logic
finite model finding

Metrics

Access Statistics
Total Accesses (updated on a weekly basis)

0

Document

0

Metadata

Abstract

In this paper we deal with verification of safety properties of term-rewriting systems. The verification problem is translated to a purely logical problem of finding a finite countermodel for a first-order formula, which is further resolved by a generic finite model finding procedure. A finite countermodel produced during successful verification provides with a concise description of the system invariant sufficient to demonstrate a specific safety property. 

We show the relative completeness of this approach with respect to the tree automata completion technique. On a set of examples taken from the literature we demonstrate the efficiency of finite model finding approach as well as its explanatory power.

Cite As Get BibTex

Alexei Lisitsa. Finite Models vs Tree Automata in Safety Verification. In 23rd International Conference on Rewriting Techniques and Applications (RTA'12). Leibniz International Proceedings in Informatics (LIPIcs), Volume 15, pp. 225-239, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2012) https://doi.org/10.4230/LIPIcs.RTA.2012.225

Author Details

Alexei Lisitsa

Any Issues?

Feedback on the Current Page

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail