84 Search Results for "Schewe, Sven"


Volume

LIPIcs, Volume 118

29th International Conference on Concurrency Theory (CONCUR 2018)

CONCUR 2018, September 4-7, 2018, Beijing, China

Editors: Sven Schewe and Lijun Zhang

Volume

LIPIcs, Volume 90

24th International Symposium on Temporal Representation and Reasoning (TIME 2017)

TIME 2017, October 16-18, 2017, Mons, Belgium

Editors: Sven Schewe, Thomas Schneider, and Jef Wijsen

Document
Deciding What Is Good-For-MDPs

Authors: Sven Schewe, Qiyi Tang, and Tansholpan Zhanabekova

Published in: LIPIcs, Volume 279, 34th International Conference on Concurrency Theory (CONCUR 2023)


Abstract
Nondeterministic good-for-MDPs (GFM) automata are for MDP model checking and reinforcement learning what good-for-games automata are for reactive synthesis: a more compact alternative to deterministic automata that displays nondeterminism, but only so much that it can be resolved locally, such that a syntactic product can be analysed. GFM has recently been introduced as a property for reinforcement learning, where the simpler Büchi acceptance conditions it allows to use is key. However, while there are classic and novel techniques to obtain automata that are GFM, there has not been a decision procedure for checking whether or not an automaton is GFM. We show that GFM-ness is decidable and provide an EXPTIME decision procedure as well as a PSPACE-hardness proof.

Cite as

Sven Schewe, Qiyi Tang, and Tansholpan Zhanabekova. Deciding What Is Good-For-MDPs. In 34th International Conference on Concurrency Theory (CONCUR 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 279, pp. 35:1-35:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)


Copy BibTex To Clipboard

@InProceedings{schewe_et_al:LIPIcs.CONCUR.2023.35,
  author =	{Schewe, Sven and Tang, Qiyi and Zhanabekova, Tansholpan},
  title =	{{Deciding What Is Good-For-MDPs}},
  booktitle =	{34th International Conference on Concurrency Theory (CONCUR 2023)},
  pages =	{35:1--35:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-299-0},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{279},
  editor =	{P\'{e}rez, Guillermo A. and Raskin, Jean-Fran\c{c}ois},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2023.35},
  URN =		{urn:nbn:de:0030-drops-190290},
  doi =		{10.4230/LIPIcs.CONCUR.2023.35},
  annote =	{Keywords: B\"{u}chi automata, Markov Decision Processes, Omega-regular objectives, Reinforcement learning}
}
Document
Singly Exponential Translation of Alternating Weak Büchi Automata to Unambiguous Büchi Automata

Authors: Yong Li, Sven Schewe, and Moshe Y. Vardi

Published in: LIPIcs, Volume 279, 34th International Conference on Concurrency Theory (CONCUR 2023)


Abstract
We introduce a method for translating an alternating weak Büchi automaton (AWA), which corresponds to a Linear Dynamic Logic (LDL) formula, to an unambiguous Büchi automaton (UBA). Our translations generalise constructions for Linear Temporal Logic (LTL), a less expressive specification language than LDL. In classical constructions, LTL formulas are first translated to alternating very weak automata (AVAs) - automata that have only singleton strongly connected components (SCCs); the AVAs are then handled by efficient disambiguation procedures. However, general AWAs can have larger SCCs, which complicates disambiguation. Currently, the only available disambiguation procedure has to go through an intermediate construction of nondeterministic Büchi automata (NBAs), which would incur an exponential blow-up of its own. We introduce a translation from general AWAs to UBAs with a singly exponential blow-up, which also immediately provides a singly exponential translation from LDL to UBAs. Interestingly, the complexity of our translation is smaller than the best known disambiguation algorithm for NBAs (broadly (0.53n)ⁿ vs. (0.76n)ⁿ), while the input of our construction can be exponentially more succinct.

Cite as

Yong Li, Sven Schewe, and Moshe Y. Vardi. Singly Exponential Translation of Alternating Weak Büchi Automata to Unambiguous Büchi Automata. In 34th International Conference on Concurrency Theory (CONCUR 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 279, pp. 37:1-37:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)


Copy BibTex To Clipboard

@InProceedings{li_et_al:LIPIcs.CONCUR.2023.37,
  author =	{Li, Yong and Schewe, Sven and Vardi, Moshe Y.},
  title =	{{Singly Exponential Translation of Alternating Weak B\"{u}chi Automata to Unambiguous B\"{u}chi Automata}},
  booktitle =	{34th International Conference on Concurrency Theory (CONCUR 2023)},
  pages =	{37:1--37:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-299-0},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{279},
  editor =	{P\'{e}rez, Guillermo A. and Raskin, Jean-Fran\c{c}ois},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2023.37},
  URN =		{urn:nbn:de:0030-drops-190313},
  doi =		{10.4230/LIPIcs.CONCUR.2023.37},
  annote =	{Keywords: B\"{u}chi automata, unambiguous automata, alternation, weak, disambiguation}
}
Document
Natural Colors of Infinite Words

Authors: Rüdiger Ehlers and Sven Schewe

Published in: LIPIcs, Volume 250, 42nd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2022)


Abstract
While finite automata have minimal DFAs as a simple and natural normal form, deterministic omega-automata do not currently have anything similar. One reason for this is that a normal form for omega-regular languages has to speak about more than acceptance - for example, to have a normal form for a parity language, it should relate every infinite word to some natural color for this language. This raises the question of whether or not a concept such as a natural color of an infinite word (for a given language) exists, and, if it does, how it relates back to automata. We define the natural color of a word purely based on an omega-regular language, and show how this natural color can be traced back from any deterministic parity automaton after two cheap and simple automaton transformations. The resulting streamlined automaton does not necessarily accept every word with its natural color, but it has a "co-run", which is like a run, but can once move to a language equivalent state, whose color is the natural color, and no co-run with a higher color exists. The streamlined automaton defines, for every color c, a good-for-games co-Büchi automaton that recognizes the words whose natural colors with respect to the represented language are at least c. This provides a canonical representation for every ω-regular language, because good-for-games co-Büchi automata have a canonical minimal - and cheap to obtain - representation for every co-Büchi language.

Cite as

Rüdiger Ehlers and Sven Schewe. Natural Colors of Infinite Words. In 42nd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 250, pp. 36:1-36:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)


Copy BibTex To Clipboard

@InProceedings{ehlers_et_al:LIPIcs.FSTTCS.2022.36,
  author =	{Ehlers, R\"{u}diger and Schewe, Sven},
  title =	{{Natural Colors of Infinite Words}},
  booktitle =	{42nd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2022)},
  pages =	{36:1--36:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-261-7},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{250},
  editor =	{Dawar, Anuj and Guruswami, Venkatesan},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2022.36},
  URN =		{urn:nbn:de:0030-drops-174280},
  doi =		{10.4230/LIPIcs.FSTTCS.2022.36},
  annote =	{Keywords: parity automata, automata over infinite words, \omega-regular languages}
}
Document
Minimising Good-For-Games Automata Is NP-Complete

Authors: Sven Schewe

Published in: LIPIcs, Volume 182, 40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2020)


Abstract
This paper discusses the hardness of finding minimal good-for-games (GFG) Büchi, Co-Büchi, and parity automata with state based acceptance. The problem appears to sit between finding small deterministic and finding small nondeterministic automata, where minimality is NP-complete and PSPACE-complete, respectively. However, recent work of Radi and Kupferman has shown that minimising Co-Büchi automata with transition based acceptance is tractable, which suggests that the complexity of minimising GFG automata might be cheaper than minimising deterministic automata. We show for the standard state based acceptance that the minimality of a GFG automaton is NP-complete for Büchi, Co-Büchi, and parity GFG automata. The proofs are a surprisingly straight forward generalisation of the proofs from deterministic Büchi automata: they use a similar reductions, and the same hard class of languages.

Cite as

Sven Schewe. Minimising Good-For-Games Automata Is NP-Complete. In 40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 182, pp. 56:1-56:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)


Copy BibTex To Clipboard

@InProceedings{schewe:LIPIcs.FSTTCS.2020.56,
  author =	{Schewe, Sven},
  title =	{{Minimising Good-For-Games Automata Is NP-Complete}},
  booktitle =	{40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2020)},
  pages =	{56:1--56:13},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-174-0},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{182},
  editor =	{Saxena, Nitin and Simon, Sunil},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2020.56},
  URN =		{urn:nbn:de:0030-drops-132973},
  doi =		{10.4230/LIPIcs.FSTTCS.2020.56},
  annote =	{Keywords: Good-for-Games Automata, Automata Minimisation}
}
Document
Model-Free Reinforcement Learning for Stochastic Parity Games

Authors: Ernst Moritz Hahn, Mateo Perez, Sven Schewe, Fabio Somenzi, Ashutosh Trivedi, and Dominik Wojtczak

Published in: LIPIcs, Volume 171, 31st International Conference on Concurrency Theory (CONCUR 2020)


Abstract
This paper investigates the use of model-free reinforcement learning to compute the optimal value in two-player stochastic games with parity objectives. In this setting, two decision makers, player Min and player Max, compete on a finite game arena - a stochastic game graph with unknown but fixed probability distributions - to minimize and maximize, respectively, the probability of satisfying a parity objective. We give a reduction from stochastic parity games to a family of stochastic reachability games with a parameter ε, such that the value of a stochastic parity game equals the limit of the values of the corresponding simple stochastic games as the parameter ε tends to 0. Since this reduction does not require the knowledge of the probabilistic transition structure of the underlying game arena, model-free reinforcement learning algorithms, such as minimax Q-learning, can be used to approximate the value and mutual best-response strategies for both players in the underlying stochastic parity game. We also present a streamlined reduction from 1 1/2-player parity games to reachability games that avoids recourse to nondeterminism. Finally, we report on the experimental evaluations of both reductions.

Cite as

Ernst Moritz Hahn, Mateo Perez, Sven Schewe, Fabio Somenzi, Ashutosh Trivedi, and Dominik Wojtczak. Model-Free Reinforcement Learning for Stochastic Parity Games. In 31st International Conference on Concurrency Theory (CONCUR 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 171, pp. 21:1-21:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)


Copy BibTex To Clipboard

@InProceedings{hahn_et_al:LIPIcs.CONCUR.2020.21,
  author =	{Hahn, Ernst Moritz and Perez, Mateo and Schewe, Sven and Somenzi, Fabio and Trivedi, Ashutosh and Wojtczak, Dominik},
  title =	{{Model-Free Reinforcement Learning for Stochastic Parity Games}},
  booktitle =	{31st International Conference on Concurrency Theory (CONCUR 2020)},
  pages =	{21:1--21:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-160-3},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{171},
  editor =	{Konnov, Igor and Kov\'{a}cs, Laura},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2020.21},
  URN =		{urn:nbn:de:0030-drops-128332},
  doi =		{10.4230/LIPIcs.CONCUR.2020.21},
  annote =	{Keywords: Reinforcement learning, Stochastic games, Omega-regular objectives}
}
Document
Complete Volume
LIPIcs, Volume 118, CONCUR'18, Complete Volume

Authors: Sven Schewe and Lijun Zhang

Published in: LIPIcs, Volume 118, 29th International Conference on Concurrency Theory (CONCUR 2018)


Abstract
LIPIcs, Volume 118, CONCUR'18, Complete Volume

Cite as

29th International Conference on Concurrency Theory (CONCUR 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 118, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)


Copy BibTex To Clipboard

@Proceedings{schewe_et_al:LIPIcs.CONCUR.2018,
  title =	{{LIPIcs, Volume 118, CONCUR'18, Complete Volume}},
  booktitle =	{29th International Conference on Concurrency Theory (CONCUR 2018)},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-087-3},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{118},
  editor =	{Schewe, Sven and Zhang, Lijun},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2018},
  URN =		{urn:nbn:de:0030-drops-97431},
  doi =		{10.4230/LIPIcs.CONCUR.2018},
  annote =	{Keywords: Theory of Computation}
}
Document
Front Matter
Front Matter, Table of Contents, Preface, Conference Organization

Authors: Sven Schewe and Lijun Zhang

Published in: LIPIcs, Volume 118, 29th International Conference on Concurrency Theory (CONCUR 2018)


Abstract
Front Matter, Table of Contents, Preface, Conference Organization

Cite as

29th International Conference on Concurrency Theory (CONCUR 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 118, pp. 0:i-0:xxi, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)


Copy BibTex To Clipboard

@InProceedings{schewe_et_al:LIPIcs.CONCUR.2018.0,
  author =	{Schewe, Sven and Zhang, Lijun},
  title =	{{Front Matter, Table of Contents, Preface, Conference Organization}},
  booktitle =	{29th International Conference on Concurrency Theory (CONCUR 2018)},
  pages =	{0:i--0:xxi},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-087-3},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{118},
  editor =	{Schewe, Sven and Zhang, Lijun},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2018.0},
  URN =		{urn:nbn:de:0030-drops-95386},
  doi =		{10.4230/LIPIcs.CONCUR.2018.0},
  annote =	{Keywords: Front Matter, Table of Contents, Preface, Conference Organization}
}
Document
Invited Talk
The Siren Song of Temporal Synthesis (Invited Talk)

Authors: Moshe Y. Vardi

Published in: LIPIcs, Volume 118, 29th International Conference on Concurrency Theory (CONCUR 2018)


Abstract
One of the most significant developments in the area of design verification over the last three decade is the development of algorithmic methods for verifying temporal specification of finite-state designs. A frequent criticism against this approach, however, is that verification is done after significant resources have already been invested in the development of the design. Since designs invariably contains errors, verification simply becomes part of the debugging process. The critics argue that the desired goal is to use temporal specification in the design development process in order to guarantee the development of correct designs. This is called temporal synthesis. In this talk I will review 60 years of research on the temporal synthesis problem, describe the automata-theoretic approach developed to solve this problem, and describe both successes and failures of this research program [Zhu et al., 2017a and 2017b].

Cite as

Moshe Y. Vardi. The Siren Song of Temporal Synthesis (Invited Talk). In 29th International Conference on Concurrency Theory (CONCUR 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 118, p. 1:1, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)


Copy BibTex To Clipboard

@InProceedings{vardi:LIPIcs.CONCUR.2018.1,
  author =	{Vardi, Moshe Y.},
  title =	{{The Siren Song of Temporal Synthesis}},
  booktitle =	{29th International Conference on Concurrency Theory (CONCUR 2018)},
  pages =	{1:1--1:1},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-087-3},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{118},
  editor =	{Schewe, Sven and Zhang, Lijun},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2018.1},
  URN =		{urn:nbn:de:0030-drops-95393},
  doi =		{10.4230/LIPIcs.CONCUR.2018.1},
  annote =	{Keywords: Formal Methods, Temporal Synthesis}
}
Document
Invited Paper
Bisimulations for Probabilistic and Quantum Processes (Invited Paper)

Authors: Yuxin Deng

Published in: LIPIcs, Volume 118, 29th International Conference on Concurrency Theory (CONCUR 2018)


Abstract
Bisimulation is a fundamental concept in the classical concurrency theory for comparing the behaviour of nondeterministic processes. It admits elegant characterisations from various perspectives such as fixed point theory, modal logics, game theory, coalgebras etc. In this paper, we review some key ideas used in the formulations and characterisations of reasonable notions of bisimulations for both probabilistic and quantum processes. To some extent the transition from probabilistic to quantum concurrency theory is smooth and natural. However, new ideas need also to be introduced. We have not yet reached the stage of formally verifying quantum communication protocols and quantum algorithms using bisimulations implemented by automatic tools. We discuss some recent efforts in this direction.

Cite as

Yuxin Deng. Bisimulations for Probabilistic and Quantum Processes (Invited Paper). In 29th International Conference on Concurrency Theory (CONCUR 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 118, pp. 2:1-2:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)


Copy BibTex To Clipboard

@InProceedings{deng:LIPIcs.CONCUR.2018.2,
  author =	{Deng, Yuxin},
  title =	{{Bisimulations for Probabilistic and Quantum Processes}},
  booktitle =	{29th International Conference on Concurrency Theory (CONCUR 2018)},
  pages =	{2:1--2:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-087-3},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{118},
  editor =	{Schewe, Sven and Zhang, Lijun},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2018.2},
  URN =		{urn:nbn:de:0030-drops-95406},
  doi =		{10.4230/LIPIcs.CONCUR.2018.2},
  annote =	{Keywords: Bisimulations, probabilistic processes, quantum processes}
}
Document
Invited Talk
Is Speed-Independent Mutual Exclusion Implementable? (Invited Talk)

Authors: Rob van Glabbeek

Published in: LIPIcs, Volume 118, 29th International Conference on Concurrency Theory (CONCUR 2018)


Abstract
A mutual exclusion algorithm is called speed independent if its correctness does not depend on the relative speed of the components. Famous mutual exclusion protocols such as Dekker's, Peterson's and Lamport's bakery are meant to be speed independent. In this talk I argue that speed-independent mutual exclusion may not be implementable on standard hardware, depending on how we believe reading and writing to a memory location is really carried out. It can be implemented on electrical circuits, however. This builds on previous work showing that mutual exclusion cannot be accurately modelled in standard process algebras.

Cite as

Rob van Glabbeek. Is Speed-Independent Mutual Exclusion Implementable? (Invited Talk). In 29th International Conference on Concurrency Theory (CONCUR 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 118, p. 3:1, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)


Copy BibTex To Clipboard

@InProceedings{vanglabbeek:LIPIcs.CONCUR.2018.3,
  author =	{van Glabbeek, Rob},
  title =	{{Is Speed-Independent Mutual Exclusion Implementable?}},
  booktitle =	{29th International Conference on Concurrency Theory (CONCUR 2018)},
  pages =	{3:1--3:1},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-087-3},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{118},
  editor =	{Schewe, Sven and Zhang, Lijun},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2018.3},
  URN =		{urn:nbn:de:0030-drops-95415},
  doi =		{10.4230/LIPIcs.CONCUR.2018.3},
  annote =	{Keywords: Mutual exclusion, speed independence, concurrent reading and writing, liveness, justness}
}
Document
Invited Talk
Verifying Arithmetic Assembly Programs in Cryptographic Primitives (Invited Talk)

Authors: Andy Polyakov, Ming-Hsien Tsai, Bow-Yaw Wang, and Bo-Yin Yang

Published in: LIPIcs, Volume 118, 29th International Conference on Concurrency Theory (CONCUR 2018)


Abstract
Arithmetic over large finite fields is indispensable in modern cryptography. For efficienty, these operations are often implemented in manually optimized assembly programs. Since these arithmetic assembly programs necessarily perform lots of non-linear computation, checking their correctness is a challenging verification problem. We develop techniques to verify such programs automatically in this paper. Using our techniques, we have successfully verified a number of assembly programs in OpenSSL. Moreover, our tool verifies the boringSSL Montgomery Ladderstep (about 1400 assembly instructions) in 1 hour. This is by far the fastest verification technique for such programs.

Cite as

Andy Polyakov, Ming-Hsien Tsai, Bow-Yaw Wang, and Bo-Yin Yang. Verifying Arithmetic Assembly Programs in Cryptographic Primitives (Invited Talk). In 29th International Conference on Concurrency Theory (CONCUR 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 118, pp. 4:1-4:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)


Copy BibTex To Clipboard

@InProceedings{polyakov_et_al:LIPIcs.CONCUR.2018.4,
  author =	{Polyakov, Andy and Tsai, Ming-Hsien and Wang, Bow-Yaw and Yang, Bo-Yin},
  title =	{{Verifying Arithmetic Assembly Programs in Cryptographic Primitives}},
  booktitle =	{29th International Conference on Concurrency Theory (CONCUR 2018)},
  pages =	{4:1--4:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-087-3},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{118},
  editor =	{Schewe, Sven and Zhang, Lijun},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2018.4},
  URN =		{urn:nbn:de:0030-drops-95425},
  doi =		{10.4230/LIPIcs.CONCUR.2018.4},
  annote =	{Keywords: Formal verification, Cryptography, Assembly Programs}
}
Document
Invited Tutorial
Coalgebraic Theory of Büchi and Parity Automata: Fixed-Point Specifications, Categorically (Invited Tutorial)

Authors: Ichiro Hasuo

Published in: LIPIcs, Volume 118, 29th International Conference on Concurrency Theory (CONCUR 2018)


Abstract
Coalgebra is a categorical modeling of state-based dynamics. Final coalgebras - as categorical greatest fixed points - play a central role in the theory; somewhat analogously, most coalgebraic proof techniques have been devoted to greatest fixed-point properties such as safety and bisimilarity. In this tutorial, I introduce our recent coalgebraic framework that accommodates those fixed-point specifications which are not necessarily the greatest. It does so specifically by characterizing the accepted languages of Büchi and parity automata in categorical terms. We present two characterizations of accepted languages. The proof for their coincidence offers a unique categorical perspective of the correspondence between (logical) fixed-point specifications and the (combinatorial) parity acceptance condition.

Cite as

Ichiro Hasuo. Coalgebraic Theory of Büchi and Parity Automata: Fixed-Point Specifications, Categorically (Invited Tutorial). In 29th International Conference on Concurrency Theory (CONCUR 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 118, pp. 5:1-5:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)


Copy BibTex To Clipboard

@InProceedings{hasuo:LIPIcs.CONCUR.2018.5,
  author =	{Hasuo, Ichiro},
  title =	{{Coalgebraic Theory of B\"{u}chi and Parity Automata: Fixed-Point Specifications, Categorically}},
  booktitle =	{29th International Conference on Concurrency Theory (CONCUR 2018)},
  pages =	{5:1--5:2},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-087-3},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{118},
  editor =	{Schewe, Sven and Zhang, Lijun},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2018.5},
  URN =		{urn:nbn:de:0030-drops-95430},
  doi =		{10.4230/LIPIcs.CONCUR.2018.5},
  annote =	{Keywords: Coalgebra, category theory, fixed-point logic, automata, B\"{u}chi automata, parity automata}
}
Document
Universal Safety for Timed Petri Nets is PSPACE-complete

Authors: Parosh Aziz Abdulla, Mohamed Faouzi Atig, Radu Ciobanu, Richard Mayr, and Patrick Totzke

Published in: LIPIcs, Volume 118, 29th International Conference on Concurrency Theory (CONCUR 2018)


Abstract
A timed network consists of an arbitrary number of initially identical 1-clock timed automata, interacting via hand-shake communication. In this setting there is no unique central controller, since all automata are initially identical. We consider the universal safety problem for such controller-less timed networks, i.e., verifying that a bad event (enabling some given transition) is impossible regardless of the size of the network. This universal safety problem is dual to the existential coverability problem for timed-arc Petri nets, i.e., does there exist a number m of tokens, such that starting with m tokens in a given place, and none in the other places, some given transition is eventually enabled. We show that these problems are PSPACE-complete.

Cite as

Parosh Aziz Abdulla, Mohamed Faouzi Atig, Radu Ciobanu, Richard Mayr, and Patrick Totzke. Universal Safety for Timed Petri Nets is PSPACE-complete. In 29th International Conference on Concurrency Theory (CONCUR 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 118, pp. 6:1-6:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)


Copy BibTex To Clipboard

@InProceedings{abdulla_et_al:LIPIcs.CONCUR.2018.6,
  author =	{Abdulla, Parosh Aziz and Atig, Mohamed Faouzi and Ciobanu, Radu and Mayr, Richard and Totzke, Patrick},
  title =	{{Universal Safety for Timed Petri Nets is PSPACE-complete}},
  booktitle =	{29th International Conference on Concurrency Theory (CONCUR 2018)},
  pages =	{6:1--6:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-087-3},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{118},
  editor =	{Schewe, Sven and Zhang, Lijun},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2018.6},
  URN =		{urn:nbn:de:0030-drops-95447},
  doi =		{10.4230/LIPIcs.CONCUR.2018.6},
  annote =	{Keywords: timed networks, safety checking, Petri nets, coverability}
}
  • Refine by Author
  • 17 Schewe, Sven
  • 4 Zhang, Lijun
  • 3 Cairo, Massimo
  • 3 Esparza, Javier
  • 3 König, Barbara
  • Show More...

  • Refine by Classification
  • 12 Theory of computation → Logic and verification
  • 10 Theory of computation → Automata over infinite objects
  • 5 Theory of computation → Timed and hybrid models
  • 4 Theory of computation → Concurrency
  • 3 Mathematics of computing → Markov processes
  • Show More...

  • Refine by Keyword
  • 4 Büchi automata
  • 4 Petri nets
  • 3 Reinforcement learning
  • 3 Temporal Logic
  • 3 automata
  • Show More...

  • Refine by Type
  • 82 document
  • 2 volume

  • Refine by Publication Year
  • 47 2018
  • 26 2017
  • 2 2010
  • 2 2020
  • 2 2023
  • Show More...

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