4 Search Results for "To, Anthony Widjaja"

Document
DOI: 10.4230/LIPIcs.CSL.2024.46
Concurrent Stochastic Lossy Channel Games

Authors: Daniel Stan, Muhammad Najib, Anthony Widjaja Lin, and Parosh Aziz Abdulla

Published in: LIPIcs, Volume 288, 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024)

Abstract
Concurrent stochastic games are an important formalism for the rational verification of probabilistic multi-agent systems, which involves verifying whether a temporal logic property is satisfied in some or all game-theoretic equilibria of such systems. In this work, we study the rational verification of probabilistic multi-agent systems where agents can cooperate by communicating over unbounded lossy channels. To model such systems, we present concurrent stochastic lossy channel games (CSLCG) and employ an equilibrium concept from cooperative game theory known as the core, which is the most fundamental and widely studied cooperative equilibrium concept. Our main contribution is twofold. First, we show that the rational verification problem is undecidable for systems whose agents have almost-sure LTL objectives. Second, we provide a decidable fragment of such a class of objectives that subsumes almost-sure reachability and safety. Our techniques involve reductions to solving infinite-state zero-sum games with conjunctions of qualitative objectives. To the best of our knowledge, our result represents the first decidability result on the rational verification of stochastic multi-agent systems on infinite arenas.
Cite as

Daniel Stan, Muhammad Najib, Anthony Widjaja Lin, and Parosh Aziz Abdulla. Concurrent Stochastic Lossy Channel Games. In 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 288, pp. 46:1-46:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{stan_et_al:LIPIcs.CSL.2024.46,
  author =	{Stan, Daniel and Najib, Muhammad and Lin, Anthony Widjaja and Abdulla, Parosh Aziz},
  title =	{{Concurrent Stochastic Lossy Channel Games}},
  booktitle =	{32nd EACSL Annual Conference on Computer Science Logic (CSL 2024)},
  pages =	{46:1--46:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-310-2},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{288},
  editor =	{Murano, Aniello and Silva, Alexandra},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2024.46},
  URN =		{urn:nbn:de:0030-drops-196894},
  doi =		{10.4230/LIPIcs.CSL.2024.46},
  annote =	{Keywords: concurrent, games, stochastic, lossy channels, wqo, finite attractor property, cooperative, core, Nash equilibrium}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2012.313
Accelerating tree-automatic relations

Authors: Anthony Widjaja Lin

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

Abstract
We study the problem of computing the transitive closure of tree-automatic (binary) relations, which are represented by tree automata. Such relations include classes of infinite systems generated by pushdown systems (PDS), ground tree rewrite systems (GTRS), PA-processes, and Turing machines, to name a few. Although this problem is unsolvable in general, we provide a semi-algorithm for the problem and prove completeness guarantee for PDS, GTRS, and PA-processes. The semi-algorithm is an extension of a known semi-algorithm for structure-preserving tree-automatic relations, for which completeness is guaranteed for several interesting parameterized systems over tree topology. Hence, there is a single generic procedure that solves reachability for PDS, GTRS, PA-processes, and several parameterized systems in a uniform way. As an application, we provide a single generic semi-algorithm for checking repeated reachability over tree-automatic relations, for which completeness is guaranteed for the aforementioned classes.
Cite as

Anthony Widjaja Lin. Accelerating tree-automatic relations. In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2012). Leibniz International Proceedings in Informatics (LIPIcs), Volume 18, pp. 313-324, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2012)

Copy BibTex To Clipboard

@InProceedings{lin:LIPIcs.FSTTCS.2012.313,
  author =	{Lin, Anthony Widjaja},
  title =	{{Accelerating tree-automatic relations}},
  booktitle =	{IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2012)},
  pages =	{313--324},
  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.313},
  URN =		{urn:nbn:de:0030-drops-38691},
  doi =		{10.4230/LIPIcs.FSTTCS.2012.313},
  annote =	{Keywords: Semi-algorithm, Model Checking, Infinite Systems, Automata}
}
Document
DOI: 10.4230/LIPIcs.STACS.2012.148
Concurrency Makes Simple Theories Hard

Authors: Stefan Göller and Anthony Widjaja Lin

Published in: LIPIcs, Volume 14, 29th International Symposium on Theoretical Aspects of Computer Science (STACS 2012)

Abstract
A standard way of building concurrent systems is by composing several individual processes by product operators. We show that even the simplest notion of product operators (i.e. asynchronous products) suffices to increase the complexity of model checking simple logics like Hennessy-Milner (HM) logic and its extension with the reachability operator (EF-logic) from PSPACE to nonelementary. In particular, this nonelementary jump happens for EF-logic when we consider individual processes represented by pushdown systems (indeed, even with only one control state). Using this result, we prove nonelementary lower bounds on the size of formula decompositions provided by Feferman-Vaught (de)compositional methods for HM and EF logics, which reduce theories of asynchronous products to theories of the components. Finally, we show that the same nonelementary lower bounds also hold when we consider the relativization of such compositional methods to finite systems.
Cite as

Stefan Göller and Anthony Widjaja Lin. Concurrency Makes Simple Theories Hard. In 29th International Symposium on Theoretical Aspects of Computer Science (STACS 2012). Leibniz International Proceedings in Informatics (LIPIcs), Volume 14, pp. 148-159, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2012)

Copy BibTex To Clipboard

@InProceedings{goller_et_al:LIPIcs.STACS.2012.148,
  author =	{G\"{o}ller, Stefan and Widjaja Lin, Anthony},
  title =	{{Concurrency Makes Simple Theories Hard}},
  booktitle =	{29th International Symposium on Theoretical Aspects of Computer Science (STACS 2012)},
  pages =	{148--159},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-35-4},
  ISSN =	{1868-8969},
  year =	{2012},
  volume =	{14},
  editor =	{D\"{u}rr, Christoph and Wilke, Thomas},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2012.148},
  URN =		{urn:nbn:de:0030-drops-34214},
  doi =		{10.4230/LIPIcs.STACS.2012.148},
  annote =	{Keywords: Modal Logic, Model Checking, Asynchronous Product, Pushdown Systems, Feferman-Vaught, Nonelementary lower bounds}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2010.228
The Complexity of Model Checking (Collapsible) Higher-Order Pushdown Systems

Authors: Matthew Hague and Anthony Widjaja To

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

Abstract
We study (collapsible) higher-order pushdown systems --- theoretically robust and well-studied models of higher-order programs --- along with their natural subclass called (collapsible) higher-order basic process algebras. We provide a comprehensive analysis of the model checking complexity of a range of both branching-time and linear-time temporal logics. We obtain tight bounds on data, expression, and combined-complexity for both (collapsible) higher-order pushdown systems and (collapsible) higher-order basic process algebra. At order-$k$, results range from polynomial to $(k+1)$-exponential time. Finally, we study (collapsible) higher-order basic process algebras as graph generators and show that they are almost as powerful as (collapsible) higher-order pushdown systems up to MSO interpretations.
Cite as

Matthew Hague and Anthony Widjaja To. The Complexity of Model Checking (Collapsible) Higher-Order Pushdown Systems. In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2010). Leibniz International Proceedings in Informatics (LIPIcs), Volume 8, pp. 228-239, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2010)

Copy BibTex To Clipboard

@InProceedings{hague_et_al:LIPIcs.FSTTCS.2010.228,
  author =	{Hague, Matthew and To, Anthony Widjaja},
  title =	{{The Complexity of Model Checking (Collapsible) Higher-Order Pushdown Systems}},
  booktitle =	{IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2010)},
  pages =	{228--239},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-23-1},
  ISSN =	{1868-8969},
  year =	{2010},
  volume =	{8},
  editor =	{Lodaya, Kamal and Mahajan, Meena},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2010.228},
  URN =		{urn:nbn:de:0030-drops-28663},
  doi =		{10.4230/LIPIcs.FSTTCS.2010.228},
  annote =	{Keywords: Higher-Order, Collapsible, Pushdown Systems, Temporal Logics, Complexity, Model Checking}
}
  • Refine by Author
  • 2 Lin, Anthony Widjaja
  • 1 Abdulla, Parosh Aziz
  • 1 Göller, Stefan
  • 1 Hague, Matthew
  • 1 Najib, Muhammad
  • Show More...

  • Refine by Classification
  • 1 Theory of computation → Concurrency
  • 1 Theory of computation → Formal languages and automata theory
  • 1 Theory of computation → Solution concepts in game theory
  • 1 Theory of computation → Verification by model checking

  • Refine by Keyword
  • 3 Model Checking
  • 2 Pushdown Systems
  • 1 Asynchronous Product
  • 1 Automata
  • 1 Collapsible
  • Show More...

  • Refine by Type
  • 4 document

  • Refine by Publication Year
  • 2 2012
  • 1 2010
  • 1 2024

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