All

What are you looking for?

All
Projects
Results
Organizations

Quick search

  • Projects supported by TA ČR
  • Excellent projects
  • Projects with the highest public support
  • Current projects

Smart search

  • That is how I find a specific +word
  • That is how I leave the -word out of the results
  • “That is how I can find the whole phrase”

Register Automata with Linear Arithmetic

The result's identifiers

  • Result code in IS VaVaI

    <a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216305%3A26230%2F17%3APU127273" target="_blank" >RIV/00216305:26230/17:PU127273 - isvavai.cz</a>

  • Result on the web

    <a href="https://www.fit.vut.cz/research/publication/11431/" target="_blank" >https://www.fit.vut.cz/research/publication/11431/</a>

  • DOI - Digital Object Identifier

    <a href="http://dx.doi.org/10.1109/LICS.2017.8005111" target="_blank" >10.1109/LICS.2017.8005111</a>

Alternative languages

  • Result language

    angličtina

  • Original language name

    Register Automata with Linear Arithmetic

  • Original language description

    We propose a novel automata model over the alphabet of rational numbers, which we call register automata over the rationals (RAq). It reads a sequence of rational numbers and outputs another rational number. RAq is an extension of the well-known register automata (RA) over infinite alphabets, which are finite automata equipped with a finite number of registers/variables for storing values. Like in the standard RA, the RAq model allows both equality and ordering tests between values. It, moreover, allows to perform linear arithmetic between certain variables. The model is quite expressive: in addition to the standard RA, it also generalizes other well-known models such as affine programs and arithmetic circuits. The main feature of RA Q is that despite the use of linear arithmetic, the so-called invariant problem-a generalization of the standard non-emptiness problem-is decidable. We also investigate other natural decision problems, namely, commutativity, equivalence, and reachability. For deterministic RA Q , commutativity and equivalence are polynomial-time inter-reducible with the invariant problem.

  • Czech name

  • Czech description

Classification

  • Type

    D - Article in proceedings

  • CEP classification

  • OECD FORD branch

    10201 - Computer sciences, information science, bioinformathics (hardware development to be 2.2, social aspect to be 5.8)

Result continuities

  • Project

    Result was created during the realization of more than one project. More information in the Projects tab.

  • Continuities

    P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)

Others

  • Publication year

    2017

  • Confidentiality

    S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

Data specific for result type

  • Article name in the collection

    Proceedings of LICS'17

  • ISBN

    978-1-5090-3018-7

  • ISSN

  • e-ISSN

  • Number of pages

    12

  • Pages from-to

    1-12

  • Publisher name

    IEEE Computer Society

  • Place of publication

    Reykjavik

  • Event location

    Reykjavik

  • Event date

    Jun 20, 2017

  • Type of event by nationality

    WRD - Celosvětová akce

  • UT code for WoS article

    000425849500049