1 Search Results for "Gupta, Ekanshdeep"

Document
DOI: 10.4230/LIPIcs.FSTTCS.2019.41
The Well Structured Problem for Presburger Counter Machines

Authors: Alain Finkel and Ekanshdeep Gupta

Published in: LIPIcs, Volume 150, 39th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2019)

Abstract
We introduce the well structured problem as the question of whether a model (here a counter machine) is well structured (here for the usual ordering on integers). We show that it is undecidable for most of the (Presburger-defined) counter machines except for Affine VASS of dimension one. However, the strong well structured problem is decidable for all Presburger counter machines. While Affine VASS of dimension one are not, in general, well structured, we give an algorithm that computes the set of predecessors of a configuration; as a consequence this allows to decide the well structured problem for 1-Affine VASS.
Cite as

Alain Finkel and Ekanshdeep Gupta. The Well Structured Problem for Presburger Counter Machines. In 39th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 150, pp. 41:1-41:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{finkel_et_al:LIPIcs.FSTTCS.2019.41,
  author =	{Finkel, Alain and Gupta, Ekanshdeep},
  title =	{{The Well Structured Problem for Presburger Counter Machines}},
  booktitle =	{39th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2019)},
  pages =	{41:1--41:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-131-3},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{150},
  editor =	{Chattopadhyay, Arkadev and Gastin, Paul},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2019.41},
  URN =		{urn:nbn:de:0030-drops-116037},
  doi =		{10.4230/LIPIcs.FSTTCS.2019.41},
  annote =	{Keywords: Well structured transition systems, infinite state systems, Presburger counter machines, reachability, coverability}
}
  • Refine by Author
  • 1 Finkel, Alain
  • 1 Gupta, Ekanshdeep

  • Refine by Classification
  • 1 Theory of computation → Logic and verification
  • 1 Theory of computation → Verification by model checking

  • Refine by Keyword
  • 1 Presburger counter machines
  • 1 Well structured transition systems
  • 1 coverability
  • 1 infinite state systems
  • 1 reachability

  • Refine by Type
  • 1 document

  • Refine by Publication Year
  • 1 2019

Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact