DROPS

Document

DOI: 10.4230/LIPIcs.RTA.2012.225

Finite Models vs Tree Automata in Safety Verification

Authors: Alexei Lisitsa

Published in: LIPIcs, Volume 15, 23rd International Conference on Rewriting Techniques and Applications (RTA'12) (2012)

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

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)

Copy BibTex To Clipboard

@InProceedings{lisitsa:LIPIcs.RTA.2012.225,
  author =	{Lisitsa, Alexei},
  title =	{{Finite Models vs Tree Automata in Safety Verification}},
  booktitle =	{23rd International Conference on Rewriting Techniques and Applications (RTA'12)},
  pages =	{225--239},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-38-5},
  ISSN =	{1868-8969},
  year =	{2012},
  volume =	{15},
  editor =	{Tiwari, Ashish},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2012.225},
  URN =		{urn:nbn:de:0030-drops-34959},
  doi =		{10.4230/LIPIcs.RTA.2012.225},
  annote =	{Keywords: term-rewriting systems, safety verification, first-order logic, finite model finding}
}

Search Results

Documents authored by Lisitsa, Alexei

Finite Models vs Tree Automata in Safety Verification

Abstract

Cite as

Thanks for your feedback!

Could not send message