8 Search Results for "Hong, Chih-Duo"

Document
DOI: 10.4230/LIPIcs.CONCUR.2024.19
Computing Inductive Invariants of Regular Abstraction Frameworks

Authors: Philipp Czerner, Javier Esparza, Valentin Krasotin, and Christoph Welzel-Mohr

Published in: LIPIcs, Volume 311, 35th International Conference on Concurrency Theory (CONCUR 2024)

Abstract
Regular transition systems (RTS) are a popular formalism for modeling infinite-state systems in general, and parameterised systems in particular. In a CONCUR 22 paper, Esparza et al. introduce a novel approach to the verification of RTS, based on inductive invariants. The approach computes the intersection of all inductive invariants of a given RTS that can be expressed as CNF formulas with a bounded number of clauses, and uses it to construct an automaton recognising an overapproximation of the reachable configurations. The paper shows that the problem of deciding if the language of this automaton intersects a given regular set of unsafe configurations is in EXPSPACE and PSPACE-hard. We introduce regular abstraction frameworks, a generalisation of the approach of Esparza et al., very similar to the regular abstractions of Hong and Lin. A framework consists of a regular language of constraints, and a transducer, called the interpretation, that assigns to each constraint the set of configurations of the RTS satisfying it. Examples of regular abstraction frameworks include the formulas of Esparza et al., octagons, bounded difference matrices, and views. We show that the generalisation of the decision problem above to regular abstraction frameworks remains in EXPSPACE, and prove a matching (non-trivial) EXPSPACE-hardness bound. EXPSPACE-hardness implies that, in the worst case, the automaton recognising the overapproximation of the reachable configurations has a double-exponential number of states. We introduce a learning algorithm that computes this automaton in a lazy manner, stopping whenever the current hypothesis is already strong enough to prove safety. We report on an implementation and show that our experimental results improve on those of Esparza et al.
Cite as

Philipp Czerner, Javier Esparza, Valentin Krasotin, and Christoph Welzel-Mohr. Computing Inductive Invariants of Regular Abstraction Frameworks. In 35th International Conference on Concurrency Theory (CONCUR 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 311, pp. 19:1-19:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{czerner_et_al:LIPIcs.CONCUR.2024.19,
  author =	{Czerner, Philipp and Esparza, Javier and Krasotin, Valentin and Welzel-Mohr, Christoph},
  title =	{{Computing Inductive Invariants of Regular Abstraction Frameworks}},
  booktitle =	{35th International Conference on Concurrency Theory (CONCUR 2024)},
  pages =	{19:1--19:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-339-3},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{311},
  editor =	{Majumdar, Rupak and Silva, Alexandra},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2024.19},
  URN =		{urn:nbn:de:0030-drops-207919},
  doi =		{10.4230/LIPIcs.CONCUR.2024.19},
  annote =	{Keywords: Regular model checking, abstraction, inductive invariants}
}
Document
DOI: 10.4230/LIPIcs.SAT.2024.6
Clausal Congruence Closure

Authors: Armin Biere, Katalin Fazekas, Mathias Fleury, and Nils Froleyks

Published in: LIPIcs, Volume 305, 27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024)

Abstract
Many practical applications of satisfiability solving employ multiple steps to encode an original problem formulation into conjunctive normal form. Often circuits are used as intermediate representation before encoding those circuits into clausal form. These circuits however might contain redundant isomorphic sub-circuits. If blindly translated into clausal form, this redundancy is retained and increases solving time unless specific preprocessing algorithms are used. Furthermore, such redundant sub-formula structure might only emerge during solving and needs to be addressed by inprocessing. This paper presents a new approach which extracts gate information from the formula and applies congruence closure to match and eliminate redundant gates. Besides new algorithms for gate extraction, we also describe previous unpublished attempts to tackle this problem. Experiments focus on the important problem of combinational equivalence checking for hardware designs and show that our new approach yields a substantial gain in CNF solver performance.
Cite as

Armin Biere, Katalin Fazekas, Mathias Fleury, and Nils Froleyks. Clausal Congruence Closure. In 27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 305, pp. 6:1-6:25, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{biere_et_al:LIPIcs.SAT.2024.6,
  author =	{Biere, Armin and Fazekas, Katalin and Fleury, Mathias and Froleyks, Nils},
  title =	{{Clausal Congruence Closure}},
  booktitle =	{27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024)},
  pages =	{6:1--6:25},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-334-8},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{305},
  editor =	{Chakraborty, Supratik and Jiang, Jie-Hong Roland},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2024.6},
  URN =		{urn:nbn:de:0030-drops-205287},
  doi =		{10.4230/LIPIcs.SAT.2024.6},
  annote =	{Keywords: Satisfiability Solving, Congruence Closure, Structural Hashing, SAT Sweeping, Conjunctive Normal Form, Combinational Equivalence Checking, Hardware Equivalence Checking}
}
Document
DOI: 10.4230/LIPIcs.SAT.2024.14
Cooking String-Integer Conversions with Noodles

Authors: Vojtěch Havlena, Lukáš Holík, Ondřej Lengál, and Juraj Síč

Published in: LIPIcs, Volume 305, 27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024)

Abstract
We propose a method for efficient handling string constraints with string-integer conversions. It extends the recently introduced stabilization-based procedure for solving string (dis)equations with regular and length constraints. Our approach is to translate the conversions into a linear integer arithmetic formula, together with regular constraints and word equations. We have integrated it into the string solver Z3-Noodler, and our experiments show that it is competitive and on some established benchmarks even several orders of magnitude faster than the state of the art.
Cite as

Vojtěch Havlena, Lukáš Holík, Ondřej Lengál, and Juraj Síč. Cooking String-Integer Conversions with Noodles. In 27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 305, pp. 14:1-14:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{havlena_et_al:LIPIcs.SAT.2024.14,
  author =	{Havlena, Vojt\v{e}ch and Hol{\'\i}k, Luk\'{a}\v{s} and Leng\'{a}l, Ond\v{r}ej and S{\'\i}\v{c}, Juraj},
  title =	{{Cooking String-Integer Conversions with Noodles}},
  booktitle =	{27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024)},
  pages =	{14:1--14:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-334-8},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{305},
  editor =	{Chakraborty, Supratik and Jiang, Jie-Hong Roland},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2024.14},
  URN =		{urn:nbn:de:0030-drops-205365},
  doi =		{10.4230/LIPIcs.SAT.2024.14},
  annote =	{Keywords: string solving, string conversions, SMT solving}
}
Document
DOI: 10.4230/LIPIcs.SAT.2024.23
eSLIM: Circuit Minimization with SAT Based Local Improvement

Authors: Franz-Xaver Reichl, Friedrich Slivovsky, and Stefan Szeider

Published in: LIPIcs, Volume 305, 27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024)

Abstract
eSLIM is a tool for circuit minimization that utilizes Exact Synthesis and the SAT-based local improvement method (SLIM) to locally improve circuits. eSLIM improves upon the earlier prototype CIOPS that uses Quantified Boolean Formulas (QBF) to succinctly encode resynthesis of multi-output subcircuits subject to don't cares. This paper describes two improvements. First, it presents a purely propositional encoding based on a Boolean relation characterizing the input-output behavior of the subcircuit under don't cares. This allows the use of a SAT solver for resynthesis, substantially reducing running times when applied to functions from the IWLS 2023 competition, where eSLIM placed second. Second, it proposes circuit partitioning techniques in which don't cares for a subcircuit are captured only with respect to an enclosing window, rather than the entire circuit. Circuit partitioning trades completeness for efficiency, and successfully enables the application of exact synthesis to some of the largest circuits in the EPFL suite, leading to improvements over the current best implementation for several instances.
Cite as

Franz-Xaver Reichl, Friedrich Slivovsky, and Stefan Szeider. eSLIM: Circuit Minimization with SAT Based Local Improvement. In 27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 305, pp. 23:1-23:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{reichl_et_al:LIPIcs.SAT.2024.23,
  author =	{Reichl, Franz-Xaver and Slivovsky, Friedrich and Szeider, Stefan},
  title =	{{eSLIM: Circuit Minimization with SAT Based Local Improvement}},
  booktitle =	{27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024)},
  pages =	{23:1--23:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-334-8},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{305},
  editor =	{Chakraborty, Supratik and Jiang, Jie-Hong Roland},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2024.23},
  URN =		{urn:nbn:de:0030-drops-205458},
  doi =		{10.4230/LIPIcs.SAT.2024.23},
  annote =	{Keywords: QBF, Exact Synthesis, Circuit Minimization, SLIM}
}
Document
Track A: Algorithms, Complexity and Games
DOI: 10.4230/LIPIcs.ICALP.2024.122
An Improved Integrality Gap for Disjoint Cycles in Planar Graphs

Authors: Niklas Schlomberg

Published in: LIPIcs, Volume 297, 51st International Colloquium on Automata, Languages, and Programming (ICALP 2024)

Abstract
We present a new greedy rounding algorithm for the Cycle Packing Problem for uncrossable cycle families in planar graphs. This improves the best-known upper bound for the integrality gap of the natural packing LP to a constant slightly less than 3.5. Furthermore, the analysis works for both edge- and vertex-disjoint packing. The previously best-known constants were 4 for edge-disjoint and 5 for vertex-disjoint cycle packing. This result also immediately yields an improved Erdős-Pósa ratio: for any uncrossable cycle family in a planar graph, the minimum number of vertices (edges) needed to hit all cycles in the family is less than 8.38 times the maximum number of vertex-disjoint (edge-disjoint, respectively) cycles in the family. Some uncrossable cycle families of interest to which the result can be applied are the family of all cycles in a directed or undirected graph, in undirected graphs also the family of all odd cycles and the family of all cycles containing exactly one edge from a specified set of demand edges. The last example is an equivalent formulation of the fully planar Disjoint Paths Problem. Here the Erdős-Pósa ratio translates to a ratio between integral multi-commodity flows and minimum cuts.
Cite as

Niklas Schlomberg. An Improved Integrality Gap for Disjoint Cycles in Planar Graphs. In 51st International Colloquium on Automata, Languages, and Programming (ICALP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 297, pp. 122:1-122:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{schlomberg:LIPIcs.ICALP.2024.122,
  author =	{Schlomberg, Niklas},
  title =	{{An Improved Integrality Gap for Disjoint Cycles in Planar Graphs}},
  booktitle =	{51st International Colloquium on Automata, Languages, and Programming (ICALP 2024)},
  pages =	{122:1--122:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-322-5},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{297},
  editor =	{Bringmann, Karl and Grohe, Martin and Puppis, Gabriele and Svensson, Ola},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2024.122},
  URN =		{urn:nbn:de:0030-drops-202651},
  doi =		{10.4230/LIPIcs.ICALP.2024.122},
  annote =	{Keywords: Cycle packing, planar graphs, disjoint paths}
}
Document
Survey
DOI: 10.4230/TGDK.2.1.4
Logics for Conceptual Data Modelling: A Review

Authors: Pablo R. Fillottrani and C. Maria Keet

Published in: TGDK, Volume 2, Issue 1 (2024): Special Issue on Trends in Graph Data and Knowledge - Part 2. Transactions on Graph Data and Knowledge, Volume 2, Issue 1

Abstract
Information modelling for databases and object-oriented information systems avails of conceptual data modelling languages such as EER and UML Class Diagrams. Many attempts exist to add logical rigour to them, for various reasons and with disparate strengths. In this paper we aim to provide a structured overview of the many efforts. We focus on aims, approaches to the formalisation, including key dimensions of choice points, popular logics used, and the main relevant reasoning services. We close with current challenges and research directions.
Cite as

Pablo R. Fillottrani and C. Maria Keet. Logics for Conceptual Data Modelling: A Review. In Special Issue on Trends in Graph Data and Knowledge - Part 2. Transactions on Graph Data and Knowledge (TGDK), Volume 2, Issue 1, pp. 4:1-4:30, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@Article{fillottrani_et_al:TGDK.2.1.4,
  author =	{Fillottrani, Pablo R. and Keet, C. Maria},
  title =	{{Logics for Conceptual Data Modelling: A Review}},
  journal =	{Transactions on Graph Data and Knowledge},
  pages =	{4:1--4:30},
  ISSN =	{2942-7517},
  year =	{2024},
  volume =	{2},
  number =	{1},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/TGDK.2.1.4},
  URN =		{urn:nbn:de:0030-drops-198616},
  doi =		{10.4230/TGDK.2.1.4},
  annote =	{Keywords: Conceptual Data Modelling, EER, UML, Description Logics, OWL}
}
Document
Track B: Automata, Logic, Semantics, and Theory of Programming
DOI: 10.4230/LIPIcs.ICALP.2019.103
Monadic Decomposability of Regular Relations (Track B: Automata, Logic, Semantics, and Theory of Programming)

Authors: Pablo Barceló, Chih-Duo Hong, Xuan-Bach Le, Anthony W. Lin, and Reino Niskanen

Published in: LIPIcs, Volume 132, 46th International Colloquium on Automata, Languages, and Programming (ICALP 2019)

Abstract
Monadic decomposibility - the ability to determine whether a formula in a given logical theory can be decomposed into a boolean combination of monadic formulas - is a powerful tool for devising a decision procedure for a given logical theory. In this paper, we revisit a classical decision problem in automata theory: given a regular (a.k.a. synchronized rational) relation, determine whether it is recognizable, i.e., it has a monadic decomposition (that is, a representation as a boolean combination of cartesian products of regular languages). Regular relations are expressive formalisms which, using an appropriate string encoding, can capture relations definable in Presburger Arithmetic. In fact, their expressive power coincide with relations definable in a universal automatic structure; equivalently, those definable by finite set interpretations in WS1S (Weak Second Order Theory of One Successor). Determining whether a regular relation admits a recognizable relation was known to be decidable (and in exponential time for binary relations), but its precise complexity still hitherto remains open. Our main contribution is to fully settle the complexity of this decision problem by developing new techniques employing infinite Ramsey theory. The complexity for DFA (resp. NFA) representations of regular relations is shown to be NLOGSPACE-complete (resp. PSPACE-complete).
Cite as

Pablo Barceló, Chih-Duo Hong, Xuan-Bach Le, Anthony W. Lin, and Reino Niskanen. Monadic Decomposability of Regular Relations (Track B: Automata, Logic, Semantics, and Theory of Programming). In 46th International Colloquium on Automata, Languages, and Programming (ICALP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 132, pp. 103:1-103:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{barcelo_et_al:LIPIcs.ICALP.2019.103,
  author =	{Barcel\'{o}, Pablo and Hong, Chih-Duo and Le, Xuan-Bach and Lin, Anthony W. and Niskanen, Reino},
  title =	{{Monadic Decomposability of Regular Relations}},
  booktitle =	{46th International Colloquium on Automata, Languages, and Programming (ICALP 2019)},
  pages =	{103:1--103:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-109-2},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{132},
  editor =	{Baier, Christel and Chatzigiannakis, Ioannis and Flocchini, Paola and Leonardi, Stefano},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2019.103},
  URN =		{urn:nbn:de:0030-drops-106790},
  doi =		{10.4230/LIPIcs.ICALP.2019.103},
  annote =	{Keywords: Transducers, Automata, Synchronized Rational Relations, Ramsey Theory, Variable Independence, Automatic Structures}
}
Document
DOI: 10.4230/LIPIcs.ISAAC.2016.61
An Improved Tax Scheme for Selfish Routing

Authors: Te-Li Wang, Chih-Kuan Yeh, and Ho-Lin Chen

Published in: LIPIcs, Volume 64, 27th International Symposium on Algorithms and Computation (ISAAC 2016)

Abstract
We study the problem of routing traffic for independent selfish users in a congested network to minimize the total latency. The inefficiency of selfish routing motivates regulating the flow of the system to lower the total latency of the Nash Equilibrium by economic incentives or penalties. When applying tax to the routes, we follow the definition of [Christodoulou et al, Algorithmica, 2014] to define ePoA as the Nash total cost including tax in the taxed network over the optimal cost in the original network. We propose a simple tax scheme consisting of step functions imposed on the links. The tax scheme can be applied to routing games with parallel links, affine cost functions and single-commodity networks to lower the ePoA to at most 4/3 - epsilon, where epsilon only depends on the discrepancy between the links. We show that there exists a tax scheme in the two link case with an ePoA upperbound less than 1.192 which is almost tight. Moreover, we design another tax scheme that lowers ePoA down to 1.281 for routing games with groups of links such that links in the same group are similar to each other and groups are sufficiently different.
Cite as

Te-Li Wang, Chih-Kuan Yeh, and Ho-Lin Chen. An Improved Tax Scheme for Selfish Routing. In 27th International Symposium on Algorithms and Computation (ISAAC 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 64, pp. 61:1-61:12, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{wang_et_al:LIPIcs.ISAAC.2016.61,
  author =	{Wang, Te-Li and Yeh, Chih-Kuan and Chen, Ho-Lin},
  title =	{{An Improved Tax Scheme for Selfish Routing}},
  booktitle =	{27th International Symposium on Algorithms and Computation (ISAAC 2016)},
  pages =	{61:1--61:12},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-026-2},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{64},
  editor =	{Hong, Seok-Hee},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ISAAC.2016.61},
  URN =		{urn:nbn:de:0030-drops-68308},
  doi =		{10.4230/LIPIcs.ISAAC.2016.61},
  annote =	{Keywords: selfish routing, price of anarchy, tax}
}
  • Refine by Author
  • 1 Barceló, Pablo
  • 1 Biere, Armin
  • 1 Chen, Ho-Lin
  • 1 Czerner, Philipp
  • 1 Esparza, Javier
  • Show More...

  • Refine by Classification
  • 3 Theory of computation → Automated reasoning
  • 2 Theory of computation → Logic and verification
  • 2 Theory of computation → Regular languages
  • 1 Computing methodologies → Description logics
  • 1 Hardware → Circuit optimization
  • Show More...

  • Refine by Keyword
  • 1 Automata
  • 1 Automatic Structures
  • 1 Circuit Minimization
  • 1 Combinational Equivalence Checking
  • 1 Conceptual Data Modelling
  • Show More...

  • Refine by Type
  • 8 document

  • Refine by Publication Year
  • 6 2024
  • 1 2016
  • 1 2019

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