2 Search Results for "Heu�ner, Alexander"

Document
DOI: 10.4230/LIPIcs.FSTTCS.2012.224
Safety Verification of Communicating One-Counter Machines

Authors: Alexander Heußner, Tristan Le Gall, and Grégoire Sutre

Published in: LIPIcs, Volume 18, IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2012)

Abstract
In order to verify protocols that tag messages with integer values, we investigate the decidability of the reachability problem for systems of communicating one-counter machines. These systems consist of local one-counter machines that asynchronously communicate by exchanging the value of their counters via, a priori unbounded, FIFO channels. This model extends communicating finite-state machines (CFSM) by infinite-state local processes and an infinite message alphabet. The main result of the paper is a complete characterization of the communication topologies that have a solvable reachability question. As already CFSM exclude the possibility of automatic verification in presence of mutual communication, we also consider an under-approximative approach to the reachability problem, based on rendezvous synchronization.
Cite as

Alexander Heußner, Tristan Le Gall, and Grégoire Sutre. Safety Verification of Communicating One-Counter Machines. In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2012). Leibniz International Proceedings in Informatics (LIPIcs), Volume 18, pp. 224-235, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2012)

Copy BibTex To Clipboard

@InProceedings{heuner_et_al:LIPIcs.FSTTCS.2012.224,
  author =	{Heu{\ss}ner, Alexander and Le Gall, Tristan and Sutre, Gr\'{e}goire},
  title =	{{Safety Verification of Communicating One-Counter Machines}},
  booktitle =	{IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2012)},
  pages =	{224--235},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-47-7},
  ISSN =	{1868-8969},
  year =	{2012},
  volume =	{18},
  editor =	{D'Souza, Deepak and Radhakrishnan, Jaikumar and Telikepalli, Kavitha},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2012.224},
  URN =		{urn:nbn:de:0030-drops-38614},
  doi =		{10.4230/LIPIcs.FSTTCS.2012.224},
  annote =	{Keywords: Counter Machines, FIFO Channels, Reachability Problem, Data Words}
}
Document
DOI: 10.4230/DagSemProc.10501.3
Parsing Unary Boolean Grammars Using Online Convolution

Authors: Alexander Okhotin and Christian Reitwießner

Published in: Dagstuhl Seminar Proceedings, Volume 10501, Advances and Applications of Automata on Words and Trees (2011)

Abstract
In contrast to context-free grammars, the extension of these grammars by explicit conjunction, the so-called conjunctive grammars can generate (quite complicated) non-regular languages over a single-letter alphabet (DLT 2007). Given these expressibility results, we study the parsability of Boolean grammars, an extension of context-free grammars by conjunction and negation, over a unary alphabet and show that they can be parsed in time O(|G| log^2(n) M(n)) where M(n) is the time to multiply two n-bit integers. This multiplication algorithm is transformed into a convolution algorithm which in turn is converted to an online convolution algorithm which is used for the parsing.
Cite as

Alexander Okhotin and Christian Reitwießner. Parsing Unary Boolean Grammars Using Online Convolution. In Advances and Applications of Automata on Words and Trees. Dagstuhl Seminar Proceedings, Volume 10501, pp. 1-11, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2011)

Copy BibTex To Clipboard

@InProceedings{okhotin_et_al:DagSemProc.10501.3,
  author =	{Okhotin, Alexander and Reitwie{\ss}ner, Christian},
  title =	{{Parsing Unary Boolean Grammars Using Online Convolution}},
  booktitle =	{Advances and Applications of Automata on Words and Trees},
  pages =	{1--11},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2011},
  volume =	{10501},
  editor =	{Christian Glasser and Jean-Eric Pin and Nicole Schweikardt and Victor Selivanov and Wolfgang Thomas},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DagSemProc.10501.3},
  URN =		{urn:nbn:de:0030-drops-31465},
  doi =		{10.4230/DagSemProc.10501.3},
  annote =	{Keywords: }
}
  • Refine by Author
  • 1 Heußner, Alexander
  • 1 Le Gall, Tristan
  • 1 Okhotin, Alexander
  • 1 Reitwießner, Christian
  • 1 Sutre, Grégoire

  • Refine by Classification

  • Refine by Keyword
  • 1 Counter Machines
  • 1 Data Words
  • 1 FIFO Channels
  • 1 Reachability Problem

  • Refine by Type
  • 2 document

  • Refine by Publication Year
  • 1 2011
  • 1 2012

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