License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.FSTTCS.2017.47
URN: urn:nbn:de:0030-drops-83871
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2018/8387/
Go to the corresponding LIPIcs Volume Portal

Weinert, Alexander

VLDL Satisfiability and Model Checking via Tree Automata

pdf-format:
LIPIcs-FSTTCS-2017-47.pdf (0.6 MB)

Abstract

We present novel algorithms solving the satisfiability problem and the model checking problem for Visibly Linear Dynamic Logic (VLDL) in asymptotically optimal time via a reduction to the emptiness problem for tree automata with Büchi acceptance.
Since VLDL allows for the specification of important properties of recursive systems, this reduction enables the efficient analysis of such systems.

Furthermore, as the problem of tree automata emptiness is well-studied, this reduction enables leveraging the mature algorithms and tools for that problem in order to solve the satisfiability problem and the model checking problem for VLDL.

BibTeX - Entry

@InProceedings{weinert:LIPIcs:2018:8387,
  author =	{Alexander Weinert},
  title =	{{VLDL Satisfiability and Model Checking via Tree Automata}},
  booktitle =	{37th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2017)},
  pages =	{47:47--47:13},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-055-2},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{93},
  editor =	{Satya Lokam and R. Ramanujam},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2018/8387},
  URN =		{urn:nbn:de:0030-drops-83871},
  doi =		{10.4230/LIPIcs.FSTTCS.2017.47},
  annote =	{Keywords: Visibly Linear Dynamic Logic, Visibly Pushdown Languages, Satisfiability, Model Checking, Tree Automata}
}

Keywords: Visibly Linear Dynamic Logic, Visibly Pushdown Languages, Satisfiability, Model Checking, Tree Automata
Collection: 37th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2017)
Issue Date: 2018
Date of publication: 12.02.2018

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI