50 Search Results for "Lodaya, Kamal"

Volume

LIPIcs, Volume 8

IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2010)

FSTTCS 2010, December 15-18, 2010, Chennai, India

Editors: Kamal Lodaya and Meena Mahajan

Document
DOI: 10.4230/LIPIcs.FSTTCS.2020.55
What You Must Remember When Transforming Datawords

Authors: M. Praveen

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

Abstract
Streaming Data String Transducers (SDSTs) were introduced to model a class of imperative and a class of functional programs, manipulating lists of data items. These can be used to write commonly used routines such as insert, delete and reverse. SDSTs can handle data values from a potentially infinite data domain. The model of Streaming String Transducers (SSTs) is the fragment of SDSTs where the infinite data domain is dropped and only finite alphabets are considered. SSTs have been much studied from a language theoretical point of view. We introduce data back into SSTs, just like data was introduced to finite state automata to get register automata. The result is Streaming String Register Transducers (SSRTs), which is a subclass of SDSTs. We use origin semantics for SSRTs and give a machine independent characterization, along the lines of Myhill-Nerode theorem. Machine independent characterizations for similar models are the basis of learning algorithms and enable us to understand fragments of the models. Origin semantics of transducers track which positions of the output originate from which positions of the input. Although a restriction, using origin semantics is well justified and is known to simplify many problems related to transducers. We use origin semantics as a technical building block, in addition to characterizations of deterministic register automata. However, we need to build more on top of these to overcome some challenges unique to SSRTs.
Cite as

M. Praveen. What You Must Remember When Transforming Datawords. 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. 55:1-55:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{praveen:LIPIcs.FSTTCS.2020.55,
  author =	{Praveen, M.},
  title =	{{What You Must Remember When Transforming Datawords}},
  booktitle =	{40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2020)},
  pages =	{55:1--55:14},
  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.55},
  URN =		{urn:nbn:de:0030-drops-132967},
  doi =		{10.4230/LIPIcs.FSTTCS.2020.55},
  annote =	{Keywords: Streaming String Transducers, Data words, Machine independent characterization}
}
Document
DOI: 10.4230/LIPIcs.MFCS.2019.30
Two variable fragment of Term Modal Logic

Authors: Anantha Padmanabha and R. Ramanujam

Published in: LIPIcs, Volume 138, 44th International Symposium on Mathematical Foundations of Computer Science (MFCS 2019)

Abstract
Term modal logics (TML) are modal logics with unboundedly many modalities, with quantification over modal indices, so that we can have formulas of the form Exists y Forall x (Box_x P(x,y) implies Diamond_y P(y,x)). Like First order modal logic, TML is also "notoriously" undecidable, in the sense that even very simple fragments are undecidable. In this paper, we show the decidability of one interesting fragment, that of two variable TML. This is in contrast to two-variable First order modal logic, which is undecidable.
Cite as

Anantha Padmanabha and R. Ramanujam. Two variable fragment of Term Modal Logic. In 44th International Symposium on Mathematical Foundations of Computer Science (MFCS 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 138, pp. 30:1-30:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{padmanabha_et_al:LIPIcs.MFCS.2019.30,
  author =	{Padmanabha, Anantha and Ramanujam, R.},
  title =	{{Two variable fragment of Term Modal Logic}},
  booktitle =	{44th International Symposium on Mathematical Foundations of Computer Science (MFCS 2019)},
  pages =	{30:1--30:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-117-7},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{138},
  editor =	{Rossmanith, Peter and Heggernes, Pinar and Katoen, Joost-Pieter},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2019.30},
  URN =		{urn:nbn:de:0030-drops-109741},
  doi =		{10.4230/LIPIcs.MFCS.2019.30},
  annote =	{Keywords: Term modal logic, satisfiability problem, two variable fragment, decidability}
}
Document
DOI: 10.4230/LIPIcs.CSL.2018.28
An Algebraic Decision Procedure for Two-Variable Logic with a Between Relation

Authors: Andreas Krebs, Kamal Lodaya, Paritosh K. Pandya, and Howard Straubing

Published in: LIPIcs, Volume 119, 27th EACSL Annual Conference on Computer Science Logic (CSL 2018)

Abstract
In earlier work (LICS 2016), the authors introduced two-variable first-order logic supplemented by a binary relation that allows one to say that a letter appears between two positions. We found an effective algebraic criterion that is a necessary condition for definability in this logic, and conjectured that the criterion is also sufficient, although we proved this only in the case of two-letter alphabets. Here we prove the general conjecture. The proof is quite different from the arguments in the earlier work, and required the development of novel techniques concerning factorizations of words. We extend the results to binary relations specifying that a factor appears between two positions.
Cite as

Andreas Krebs, Kamal Lodaya, Paritosh K. Pandya, and Howard Straubing. An Algebraic Decision Procedure for Two-Variable Logic with a Between Relation. In 27th EACSL Annual Conference on Computer Science Logic (CSL 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 119, pp. 28:1-28:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{krebs_et_al:LIPIcs.CSL.2018.28,
  author =	{Krebs, Andreas and Lodaya, Kamal and Pandya, Paritosh K. and Straubing, Howard},
  title =	{{An Algebraic Decision Procedure for Two-Variable Logic with a Between Relation}},
  booktitle =	{27th EACSL Annual Conference on Computer Science Logic (CSL 2018)},
  pages =	{28:1--28:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-088-0},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{119},
  editor =	{Ghica, Dan R. and Jung, Achim},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2018.28},
  URN =		{urn:nbn:de:0030-drops-96953},
  doi =		{10.4230/LIPIcs.CSL.2018.28},
  annote =	{Keywords: two-variable logic, finite model theory, algebraic automata theory}
}
Document
Complete Volume
DOI: 10.4230/LIPIcs.FSTTCS.2010
LIPIcs, Volume 8, FSTTCS'10, Complete Volume

Authors: Kamal Lodaya and Meena Mahajan

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

Abstract
LIPIcs, Volume 8, FSTTCS'10, Complete Volume
Cite as

IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2010). Leibniz International Proceedings in Informatics (LIPIcs), Volume 8, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)

Copy BibTex To Clipboard

@Proceedings{lodaya_et_al:LIPIcs.FSTTCS.2010,
  title =	{{LIPIcs, Volume 8, FSTTCS'10, Complete Volume}},
  booktitle =	{IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2010)},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-23-1},
  ISSN =	{1868-8969},
  year =	{2013},
  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},
  URN =		{urn:nbn:de:0030-drops-41027},
  doi =		{10.4230/LIPIcs.FSTTCS.2010},
  annote =	{Keywords: Software/Program Verification, Models of Computation, Modes of Computation, Complexity Measures and Classes, Nonnumerical Algorithms and Problems pecifying and Verifying and Reasoning about Program}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2010.1
Expressiveness of streaming string transducers

Authors: Rajeev Alur and Pavol Černý

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

Abstract
Streaming string transducers define (partial) functions from input strings to output strings. A streaming string transducer makes a single pass through the input string and uses a finite set of variables that range over strings from the output alphabet. At every step, the transducer processes an input symbol, and updates all the variables in parallel using assignments whose right-hand-sides are concatenations of output symbols and variables with the restriction that a variable can be used at most once in a right-hand-side expression. It has been shown that streaming string transducers operating on strings over infinite data domains are of interest in algorithmic verification of list-processing programs, as they lead to Pspace decision procedures for checking pre/postconditions and for checking semantic equivalence, for a well-defined class of heap-manipulating programs. In order to understand the theoretical expressiveness of streaming transducers, we focus on streaming transducers processing strings over finite alphabets, given the existence of a robust and well-studied class of ``regular'' transductions for this case. Such regular transductions can be defined either by two-way deterministic finite-state transducers, or using a logical MSO-based characterization. Our main result is that the expressiveness of streaming string transducers coincides exactly with this class of regular transductions.
Cite as

Rajeev Alur and Pavol Černý. Expressiveness of streaming string transducers. In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2010). Leibniz International Proceedings in Informatics (LIPIcs), Volume 8, pp. 1-12, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2010)

Copy BibTex To Clipboard

@InProceedings{alur_et_al:LIPIcs.FSTTCS.2010.1,
  author =	{Alur, Rajeev and \v{C}ern\'{y}, Pavol},
  title =	{{Expressiveness of streaming string transducers}},
  booktitle =	{IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2010)},
  pages =	{1--12},
  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.1},
  URN =		{urn:nbn:de:0030-drops-28538},
  doi =		{10.4230/LIPIcs.FSTTCS.2010.1},
  annote =	{Keywords: streaming string transducer, list processing, heap manipulation, monadic second-order transduction}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2010.13
Special tree-width and the verification of monadic second-order graph pr operties

Authors: Bruno Courcelle

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

Abstract
The model-checking problem for monadic second-order logic on graphs is fixed-parameter tractable with respect to tree-width and clique-width. The proof constructs finite deterministic automata from monadic second-order sentences, but this computation produces automata of hyper-exponential sizes, and this is not avoidable. To overcome this difficulty, we propose to consider particular monadic second-order graph properties that are nevertheless interesting for Graph Theory and to interpret automata instead of trying to compile them (joint work with I. Durand). For checking monadic second-order sentences written with edge set quantifications, the appropriate parameter is tree-width. We introduce special tree-width, a graph complexity measure between path-width and tree-width. The corresponding automata are easier to construct than those for tree-width.
Cite as

Bruno Courcelle. Special tree-width and the verification of monadic second-order graph pr operties. In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2010). Leibniz International Proceedings in Informatics (LIPIcs), Volume 8, pp. 13-29, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2010)

Copy BibTex To Clipboard

@InProceedings{courcelle:LIPIcs.FSTTCS.2010.13,
  author =	{Courcelle, Bruno},
  title =	{{Special tree-width and the verification of monadic second-order graph pr operties}},
  booktitle =	{IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2010)},
  pages =	{13--29},
  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.13},
  URN =		{urn:nbn:de:0030-drops-28494},
  doi =		{10.4230/LIPIcs.FSTTCS.2010.13},
  annote =	{Keywords: model-checking, monadic second-order logic, fixed-parameter tractability, special tree-width}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2010.30
On extracting computations from propositional proofs (a survey)

Authors: Pavel Pudlák

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

Abstract
This paper describes a project that aims at showing that propositional proofs of certain tautologies in weak proof system give upper bounds on the computational complexity of functions associated with the tautologies. Such bounds can potentially be used to prove (conditional or unconditional) lower bounds on the lengths of proofs of these tautologies and show separations of some weak proof systems. The prototype are the results showing the feasible interpolation property for resolution. In order to prove similar results for systems stronger than resolution one needs to define suitable generalizations of boolean circuits. We will survey the known results concerning this project and sketch in which direction we want to generalize them.
Cite as

Pavel Pudlák. On extracting computations from propositional proofs (a survey). In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2010). Leibniz International Proceedings in Informatics (LIPIcs), Volume 8, pp. 30-41, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2010)

Copy BibTex To Clipboard

@InProceedings{pudlak:LIPIcs.FSTTCS.2010.30,
  author =	{Pudl\'{a}k, Pavel},
  title =	{{On extracting computations from propositional proofs (a survey)}},
  booktitle =	{IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2010)},
  pages =	{30--41},
  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.30},
  URN =		{urn:nbn:de:0030-drops-28512},
  doi =		{10.4230/LIPIcs.FSTTCS.2010.30},
  annote =	{Keywords: proof complexity, propositional tautology, boolean circuits, resolution, feasible interpolation}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2010.42
Recent Progress and Open Problems in Algorithmic Convex Geometry

Authors: Santosh S. Vempala

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

Abstract
This article is a survey of developments in algorithmic convex geometry over the past decade. These include algorithms for sampling, optimization, integration, rounding and learning, as well as mathematical tools such as isoperimetric and concentration inequalities. Several open problems and conjectures are discussed on the way.
Cite as

Santosh S. Vempala. Recent Progress and Open Problems in Algorithmic Convex Geometry. In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2010). Leibniz International Proceedings in Informatics (LIPIcs), Volume 8, pp. 42-64, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2010)

Copy BibTex To Clipboard

@InProceedings{vempala:LIPIcs.FSTTCS.2010.42,
  author =	{Vempala, Santosh S.},
  title =	{{Recent Progress and Open Problems in Algorithmic Convex Geometry}},
  booktitle =	{IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2010)},
  pages =	{42--64},
  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.42},
  URN =		{urn:nbn:de:0030-drops-28529},
  doi =		{10.4230/LIPIcs.FSTTCS.2010.42},
  annote =	{Keywords: convex geometry, geometric inequalities, algorithms, sampling, optimization, integration, rounding, learning}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2010.65
Playing in stochastic environment: from multi-armed bandits to two-player games

Authors: Wieslaw Zielonka

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

Abstract
Given a zero-sum infinite game we examine the question if players have optimal memoryless deterministic strategies. It turns out that under some general conditions the problem for two-player games can be reduced to the same problem for one-player games which in turn can be reduced to a simpler related problem for multi-armed bandits.
Cite as

Wieslaw Zielonka. Playing in stochastic environment: from multi-armed bandits to two-player games. In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2010). Leibniz International Proceedings in Informatics (LIPIcs), Volume 8, pp. 65-72, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2010)

Copy BibTex To Clipboard

@InProceedings{zielonka:LIPIcs.FSTTCS.2010.65,
  author =	{Zielonka, Wieslaw},
  title =	{{Playing in stochastic environment: from multi-armed bandits to two-player games}},
  booktitle =	{IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2010)},
  pages =	{65--72},
  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.65},
  URN =		{urn:nbn:de:0030-drops-28500},
  doi =		{10.4230/LIPIcs.FSTTCS.2010.65},
  annote =	{Keywords: two-player zero-sum game, one-player zero-sum game, multi-armed bandit, memoryless deterministic strategy}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2010.73
Better Algorithms for Satisfiability Problems for Formulas of Bounded Rank-width

Authors: Robert Ganian, Petr Hlinený, and Jan Obdrzálek

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

Abstract
We provide a parameterized polynomial algorithm for the propositional model counting problem #SAT, the runtime of which is single-exponential in the rank-width of a formula. Previously, analogous algorithms have been known --e.g. [Fischer, Makowsky, and Ravve]-- with a single-exponential dependency on the clique-width of a formula. Our algorithm thus presents an exponential runtime improvement (since clique-width reaches up to exponentially higher values than rank-width), and can be of practical interest for small values of rank-width. We also provide an algorithm for the MAX-SAT problem along the same lines.
Cite as

Robert Ganian, Petr Hlinený, and Jan Obdrzálek. Better Algorithms for Satisfiability Problems for Formulas of Bounded Rank-width. In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2010). Leibniz International Proceedings in Informatics (LIPIcs), Volume 8, pp. 73-83, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2010)

Copy BibTex To Clipboard

@InProceedings{ganian_et_al:LIPIcs.FSTTCS.2010.73,
  author =	{Ganian, Robert and Hlinen\'{y}, Petr and Obdrz\'{a}lek, Jan},
  title =	{{Better Algorithms for Satisfiability Problems for Formulas of Bounded Rank-width}},
  booktitle =	{IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2010)},
  pages =	{73--83},
  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.73},
  URN =		{urn:nbn:de:0030-drops-28541},
  doi =		{10.4230/LIPIcs.FSTTCS.2010.73},
  annote =	{Keywords: propositional model counting; satisfiability; rank-width; clique-width ; parameterized complexity}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2010.84
Satisfiability of Acyclic and Almost Acyclic CNF Formulas

Authors: Sebastian Ordyniak, Daniel Paulusma, and Stefan Szeider

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

Abstract
We study the propositional satisfiability problem (SAT) on classes of CNF formulas (formulas in Conjunctive Normal Form) that obey certain structural restrictions in terms of their hypergraph structure, by associating to a CNF formula the hypergraph obtained by ignoring negations and considering clauses as hyperedges on variables. We show that satisfiability of CNF formulas with so-called ``beta-acyclic hypergraphs'' can be decided in polynomial time. We also study the parameterized complexity of SAT for ``almost'' beta-acyclic instances, using as parameter the formula's distance from being beta-acyclic. As distance we use the size of smallest strong backdoor sets and the beta-hypertree width. As a by-product we obtain the W[1]-hardness of SAT parameterized by the (undirected) clique-width of the incidence graph, which disproves a conjecture by Fischer, Makowsky, and Ravve (Discr. Appl. Math. 156, 2008).
Cite as

Sebastian Ordyniak, Daniel Paulusma, and Stefan Szeider. Satisfiability of Acyclic and Almost Acyclic CNF Formulas. In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2010). Leibniz International Proceedings in Informatics (LIPIcs), Volume 8, pp. 84-95, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2010)

Copy BibTex To Clipboard

@InProceedings{ordyniak_et_al:LIPIcs.FSTTCS.2010.84,
  author =	{Ordyniak, Sebastian and Paulusma, Daniel and Szeider, Stefan},
  title =	{{Satisfiability of Acyclic and Almost Acyclic CNF Formulas}},
  booktitle =	{IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2010)},
  pages =	{84--95},
  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.84},
  URN =		{urn:nbn:de:0030-drops-28556},
  doi =		{10.4230/LIPIcs.FSTTCS.2010.84},
  annote =	{Keywords: Satisfiability, chordal bipartite graphs, beta-acyclic hypergraphs, backdoor sets, parameterized complexity}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2010.96
The effect of girth on the kernelization complexity of Connected Dominating Set

Authors: Neeldhara Misra, Geevarghese Philip, Venkatesh Raman, and Saket Saurabh

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

Abstract
In the Connected Dominating Set problem we are given as input a graph $G$ and a positive integer $k$, and are asked if there is a set $S$ of at most $k$ vertices of $G$ such that $S$ is a dominating set of $G$ and the subgraph induced by $S$ is connected. This is a basic connectivity problem that is known to be NP-complete, and it has been extensively studied using several algorithmic approaches. In this paper we study the effect of excluding short cycles, as a subgraph, on the kernelization complexity of Connected Dominating Set. Kernelization algorithms are polynomial-time algorithms that take an input and a positive integer $k$ (the parameter) and output an equivalent instance where the size of the new instance and the new parameter are both bounded by some function $g(k)$. The new instance is called a $g(k)$ kernel for the problem. If $g(k)$ is a polynomial in $k$ then we say that the problem admits polynomial kernels. The girth of a graph $G$ is the length of a shortest cycle in $G$. It turns out that Connected Dominating Set is ``hard'' on graphs with small cycles, and becomes progressively easier as the girth increases. More specifically, we obtain the following interesting trichotomy: Connected Dominating Set (a) does not have a kernel of any size on graphs of girth $3$ or $4$ (since the problem is W[2]-hard); (b) admits a $g(k)$ kernel, where $g(k)$ is $k^{O(k)}$, on graphs of girth $5$ or $6$ but has no polynomial kernel (unless the Polynomial Hierarchy (PH) collapses to the third level) on these graphs; (c) has a cubic ($O(k^3)$) kernel on graphs of girth at least $7$. While there is a large and growing collection of parameterized complexity results available for problems on graph classes characterized by excluded minors, our results add to the very few known in the field for graph classes characterized by excluded subgraphs.
Cite as

Neeldhara Misra, Geevarghese Philip, Venkatesh Raman, and Saket Saurabh. The effect of girth on the kernelization complexity of Connected Dominating Set. In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2010). Leibniz International Proceedings in Informatics (LIPIcs), Volume 8, pp. 96-107, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2010)

Copy BibTex To Clipboard

@InProceedings{misra_et_al:LIPIcs.FSTTCS.2010.96,
  author =	{Misra, Neeldhara and Philip, Geevarghese and Raman, Venkatesh and Saurabh, Saket},
  title =	{{The effect of girth on the kernelization complexity of Connected Dominating Set}},
  booktitle =	{IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2010)},
  pages =	{96--107},
  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.96},
  URN =		{urn:nbn:de:0030-drops-28567},
  doi =		{10.4230/LIPIcs.FSTTCS.2010.96},
  annote =	{Keywords: Connected Dominating Set, parameterized complexity, kernelization, girth}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2010.108
One-Counter Stochastic Games

Authors: Tomás Brázdil, Václav Brozek, and Kousha Etessami

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

Abstract
We study the computational complexity of basic decision problems for one-counter simple stochastic games (OC-SSGs), under various objectives. OC-SSGs are 2-player turn-based stochastic games played on the transition graph of classic one-counter automata. We study primarily the termination objective, where the goal of one player is to maximize the probability of reaching counter value 0, while the other player wishes to avoid this. Partly motivated by the goal of understanding termination objectives, we also study certain ``limit'' and ``long run average'' reward objectives that are closely related to some well-studied objectives for stochastic games with rewards. Examples of problems we address include: does player 1 have a strategy to ensure that the counter eventually hits 0, i.e., terminates, almost surely, regardless of what player 2 does? Or that the $liminf$ (or $limsup$) counter value equals $infty$ with a desired probability? Or that the long run average reward is $>0$ with desired probability? We show that the qualitative termination problem for OC-SSGs is in $NP$ intersect $coNP$, and is in P-time for 1-player OC-SSGs, or equivalently for one-counter Markov Decision Processes (OC-MDPs). Moreover, we show that quantitative limit problems for OC-SSGs are in $NP$ intersect $coNP$, and are in P-time for 1-player OC-MDPs. Both qualitative limit problems and qualitative termination problems for OC-SSGs are already at least as hard as Condon's quantitative decision problem for finite-state SSGs.
Cite as

Tomás Brázdil, Václav Brozek, and Kousha Etessami. One-Counter Stochastic Games. In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2010). Leibniz International Proceedings in Informatics (LIPIcs), Volume 8, pp. 108-119, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2010)

Copy BibTex To Clipboard

@InProceedings{brazdil_et_al:LIPIcs.FSTTCS.2010.108,
  author =	{Br\'{a}zdil, Tom\'{a}s and Brozek, V\'{a}clav and Etessami, Kousha},
  title =	{{One-Counter Stochastic Games}},
  booktitle =	{IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2010)},
  pages =	{108--119},
  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.108},
  URN =		{urn:nbn:de:0030-drops-28571},
  doi =		{10.4230/LIPIcs.FSTTCS.2010.108},
  annote =	{Keywords: one-counter automata, simple stochastic games, Markov decision process, termination, limit, long run average reward}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2010.120
ATL with Strategy Contexts: Expressiveness and Model Checking

Authors: Arnaud Da Costa, François Laroussinie, and Nicolas Markey

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

Abstract
We study the alternating-time temporal logics ATL and ATL* extended with strategy contexts: these make agents commit to their strategies during the evaluation of formulas, contrary to plain ATL and ATL* where strategy quantifiers reset previously selected strategies. We illustrate the important expressive power of strategy contexts by proving that they make the extended logics, namely ATLsc and ATLsc*, equally expressive: any formula in ATLsc* can be translated into an equivalent, linear-size ATLsc formula. Despite the high expressiveness of these logics, we~prove that their model-checking problems remain decidable by~designing a tree-automata-based algorithm for model-checking ATLsc* on the full class of $n$-player concurrent game structures.
Cite as

Arnaud Da Costa, François Laroussinie, and Nicolas Markey. ATL with Strategy Contexts: Expressiveness and Model Checking. In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2010). Leibniz International Proceedings in Informatics (LIPIcs), Volume 8, pp. 120-132, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2010)

Copy BibTex To Clipboard

@InProceedings{dacosta_et_al:LIPIcs.FSTTCS.2010.120,
  author =	{Da Costa, Arnaud and Laroussinie, Fran\c{c}ois and Markey, Nicolas},
  title =	{{ATL with Strategy Contexts: Expressiveness and Model Checking}},
  booktitle =	{IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2010)},
  pages =	{120--132},
  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.120},
  URN =		{urn:nbn:de:0030-drops-28589},
  doi =		{10.4230/LIPIcs.FSTTCS.2010.120},
  annote =	{Keywords: alternating temporal logic, agent, strategy quantifier}
}
  • Refine by Author
  • 4 Lodaya, Kamal
  • 2 Chakaravarthy, Venkatesan T.
  • 2 Mahajan, Meena
  • 2 Markey, Nicolas
  • 2 Praveen, M.
  • Show More...

  • Refine by Classification
  • 1 Theory of computation → Algebraic language theory
  • 1 Theory of computation → Automata over infinite objects
  • 1 Theory of computation → Finite Model Theory
  • 1 Theory of computation → Modal and temporal logics
  • 1 Theory of computation → Transducers

  • Refine by Keyword
  • 4 Complexity
  • 4 model-checking
  • 2 Data words
  • 2 Pushdown Systems
  • 2 alternating temporal logic
  • Show More...

  • Refine by Type
  • 49 document
  • 1 volume

  • Refine by Publication Year
  • 45 2010
  • 1 2009
  • 1 2013
  • 1 2018
  • 1 2019
  • 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
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact