54 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
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.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
Tree Automata as Algebras: Minimisation and Determinisation

Authors: Gerco van Heerdt, Tobias Kappé, Jurriaan Rot, Matteo Sammartino, and Alexandra Silva

Published in: LIPIcs, Volume 139, 8th Conference on Algebra and Coalgebra in Computer Science (CALCO 2019)


Abstract
We study a categorical generalisation of tree automata, as algebras for a fixed endofunctor endowed with initial and final states. Under mild assumptions about the base category, we present a general minimisation algorithm for these automata. We then build upon and extend an existing generalisation of the Nerode equivalence to a categorical setting and relate it to the existence of minimal automata. Finally, we show that generalised types of side-effects, such as non-determinism, can be captured by this categorical framework, leading to a general determinisation procedure.

Cite as

Gerco van Heerdt, Tobias Kappé, Jurriaan Rot, Matteo Sammartino, and Alexandra Silva. Tree Automata as Algebras: Minimisation and Determinisation. In 8th Conference on Algebra and Coalgebra in Computer Science (CALCO 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 139, pp. 6:1-6:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)


Copy BibTex To Clipboard

@InProceedings{vanheerdt_et_al:LIPIcs.CALCO.2019.6,
  author =	{van Heerdt, Gerco and Kapp\'{e}, Tobias and Rot, Jurriaan and Sammartino, Matteo and Silva, Alexandra},
  title =	{{Tree Automata as Algebras: Minimisation and Determinisation}},
  booktitle =	{8th Conference on Algebra and Coalgebra in Computer Science (CALCO 2019)},
  pages =	{6:1--6:22},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-120-7},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{139},
  editor =	{Roggenbach, Markus and Sokolova, Ana},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2019.6},
  URN =		{urn:nbn:de:0030-drops-114341},
  doi =		{10.4230/LIPIcs.CALCO.2019.6},
  annote =	{Keywords: tree automata, algebras, minimisation, determinisation, Nerode equivalence}
}
Document
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.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
Kleene Algebra with Observations

Authors: Tobias Kappé, Paul Brunet, Jurriaan Rot, Alexandra Silva, Jana Wagemaker, and Fabio Zanasi

Published in: LIPIcs, Volume 140, 30th International Conference on Concurrency Theory (CONCUR 2019)


Abstract
Kleene algebra with tests (KAT) is an algebraic framework for reasoning about the control flow of sequential programs. Generalising KAT to reason about concurrent programs is not straightforward, because axioms native to KAT in conjunction with expected axioms for concurrency lead to an anomalous equation. In this paper, we propose Kleene algebra with observations (KAO), a variant of KAT, as an alternative foundation for extending KAT to a concurrent setting. We characterise the free model of KAO, and establish a decision procedure w.r.t. its equational theory.

Cite as

Tobias Kappé, Paul Brunet, Jurriaan Rot, Alexandra Silva, Jana Wagemaker, and Fabio Zanasi. Kleene Algebra with Observations. In 30th International Conference on Concurrency Theory (CONCUR 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 140, pp. 41:1-41:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)


Copy BibTex To Clipboard

@InProceedings{kappe_et_al:LIPIcs.CONCUR.2019.41,
  author =	{Kapp\'{e}, Tobias and Brunet, Paul and Rot, Jurriaan and Silva, Alexandra and Wagemaker, Jana and Zanasi, Fabio},
  title =	{{Kleene Algebra with Observations}},
  booktitle =	{30th International Conference on Concurrency Theory (CONCUR 2019)},
  pages =	{41:1--41:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-121-4},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{140},
  editor =	{Fokkink, Wan and van Glabbeek, Rob},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2019.41},
  URN =		{urn:nbn:de:0030-drops-109431},
  doi =		{10.4230/LIPIcs.CONCUR.2019.41},
  annote =	{Keywords: Concurrent Kleene algebra, Kleene algebra with tests, free model, axiomatisation, decision procedure}
}
Document
Energy Mean-Payoff Games

Authors: Véronique Bruyère, Quentin Hautem, Mickael Randour, and Jean-François Raskin

Published in: LIPIcs, Volume 140, 30th International Conference on Concurrency Theory (CONCUR 2019)


Abstract
In this paper, we study one-player and two-player energy mean-payoff games. Energy mean-payoff games are games of infinite duration played on a finite graph with edges labeled by 2-dimensional weight vectors. The objective of the first player (the protagonist) is to satisfy an energy objective on the first dimension and a mean-payoff objective on the second dimension. We show that optimal strategies for the first player may require infinite memory while optimal strategies for the second player (the antagonist) do not require memory. In the one-player case (where only the first player has choices), the problem of deciding who is the winner can be solved in polynomial time while for the two-player case we show co-NP membership and we give effective constructions for the infinite-memory optimal strategies of the protagonist.

Cite as

Véronique Bruyère, Quentin Hautem, Mickael Randour, and Jean-François Raskin. Energy Mean-Payoff Games. In 30th International Conference on Concurrency Theory (CONCUR 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 140, pp. 21:1-21:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)


Copy BibTex To Clipboard

@InProceedings{bruyere_et_al:LIPIcs.CONCUR.2019.21,
  author =	{Bruy\`{e}re, V\'{e}ronique and Hautem, Quentin and Randour, Mickael and Raskin, Jean-Fran\c{c}ois},
  title =	{{Energy Mean-Payoff Games}},
  booktitle =	{30th International Conference on Concurrency Theory (CONCUR 2019)},
  pages =	{21:1--21:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-121-4},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{140},
  editor =	{Fokkink, Wan and van Glabbeek, Rob},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2019.21},
  URN =		{urn:nbn:de:0030-drops-109239},
  doi =		{10.4230/LIPIcs.CONCUR.2019.21},
  annote =	{Keywords: two-player zero-sum games played on graphs, energy and mean-payoff objectives, complexity study and construction of optimal strategies}
}
Document
Uniform Random Expressions Lack Expressivity

Authors: Florent Koechlin, Cyril Nicaud, and Pablo Rotondo

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


Abstract
In this article, we question the relevance of uniform random models for algorithms that use expressions as inputs. Using a general framework to describe expressions, we prove that if there is a subexpression that is absorbing for a given operator, then, after repeatedly applying the induced simplification to a uniform random expression of size n, we obtain an equivalent expression of constant expected size. This proves that uniform random expressions lack expressivity, as soon as there is an absorbing pattern. For instance, (a+b)^* is absorbing for the union for regular expressions on {a,b}, hence random regular expressions can be drastically reduced using the induced simplification.

Cite as

Florent Koechlin, Cyril Nicaud, and Pablo Rotondo. Uniform Random Expressions Lack Expressivity. In 44th International Symposium on Mathematical Foundations of Computer Science (MFCS 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 138, pp. 51:1-51:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)


Copy BibTex To Clipboard

@InProceedings{koechlin_et_al:LIPIcs.MFCS.2019.51,
  author =	{Koechlin, Florent and Nicaud, Cyril and Rotondo, Pablo},
  title =	{{Uniform Random Expressions Lack Expressivity}},
  booktitle =	{44th International Symposium on Mathematical Foundations of Computer Science (MFCS 2019)},
  pages =	{51:1--51: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.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2019.51},
  URN =		{urn:nbn:de:0030-drops-109957},
  doi =		{10.4230/LIPIcs.MFCS.2019.51},
  annote =	{Keywords: Random expressions, simplification algorithms, analytic combinatorics}
}
Document
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.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
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

Kamal Lodaya and Meena Mahajan. LIPIcs, Volume 8, FSTTCS'10, Complete Volume. In 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.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
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.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
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.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
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.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
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.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
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.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
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.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}
}
  • Refine by Author
  • 4 Lodaya, Kamal
  • 3 Silva, Alexandra
  • 2 Chakaravarthy, Venkatesan T.
  • 2 Kappé, Tobias
  • 2 Mahajan, Meena
  • Show More...

  • Refine by Classification
  • 2 Theory of computation → Formal languages and automata theory
  • 1 Mathematics of computing → Discrete mathematics
  • 1 Software and its engineering → Formal methods
  • 1 Theory of computation → Algebraic language theory
  • 1 Theory of computation → Automata over infinite objects
  • Show More...

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

  • Refine by Type
  • 53 document
  • 1 volume

  • Refine by Publication Year
  • 45 2010
  • 5 2019
  • 1 2009
  • 1 2013
  • 1 2018
  • 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