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.STACS.2017.29
URN: urn:nbn:de:0030-drops-70059
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2017/7005/
Go to the corresponding LIPIcs Volume Portal

Fijalkow, Nathanaël ; Ohlmann, Pierre ; Ouaknine, Joël ; Pouly, Amaury ; Worrell, James

Semialgebraic Invariant Synthesis for the Kannan-Lipton Orbit Problem

pdf-format:
LIPIcs-STACS-2017-29.pdf (0.5 MB)

Abstract

The Orbit Problem consists of determining, given a linear transformation A on d-dimensional rationals Q^d, together with vectors x and y, whether the orbit of x under repeated applications of A can ever reach y. This problem was famously shown to be decidable by Kannan and Lipton in the 1980s.

In this paper, we are concerned with the problem of synthesising suitable invariants P which are subsets of R^d, i.e., sets that are stable under A and contain x and not y, thereby providing compact and versatile certificates of non-reachability. We show that whether a given instance of the Orbit Problem admits a semialgebraic invariant is decidable, and moreover in positive instances we provide an algorithm to synthesise suitable invariants of polynomial size.

It is worth noting that the existence of semilinear invariants, on the other hand, is (to the best of our knowledge) not known to be decidable.

BibTeX - Entry

@InProceedings{fijalkow_et_al:LIPIcs:2017:7005,
  author =	{Nathana{\"e}l Fijalkow and Pierre Ohlmann and Jo{\"e}l Ouaknine and Amaury Pouly and James Worrell},
  title =	{{Semialgebraic Invariant Synthesis for the Kannan-Lipton Orbit Problem}},
  booktitle =	{34th Symposium on Theoretical Aspects of Computer Science (STACS 2017)},
  pages =	{29:1--29:13},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-028-6},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{66},
  editor =	{Heribert Vollmer and Brigitte Vallée},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2017/7005},
  URN =		{urn:nbn:de:0030-drops-70059},
  doi =		{10.4230/LIPIcs.STACS.2017.29},
  annote =	{Keywords: Verification,algebraic computation,Skolem Problem,Orbit Problem,invariants}
}

Keywords: Verification,algebraic computation,Skolem Problem,Orbit Problem,invariants
Collection: 34th Symposium on Theoretical Aspects of Computer Science (STACS 2017)
Issue Date: 2017
Date of publication: 06.03.2017

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