50 Search Results for "Kumar, K. Narayan"

Volume

LIPIcs, Volume 4

IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science

FSTTCS 2009, December 15-17, 2009, Kanpur, India

Editors: Ravi Kannan and K. Narayan Kumar

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.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
Track B: Automata, Logic, Semantics, and Theory of Programming
DOI: 10.4230/LIPIcs.ICALP.2020.123
The Strahler Number of a Parity Game

Authors: Laure Daviaud, Marcin Jurdziński, and K. S. Thejaswini

Published in: LIPIcs, Volume 168, 47th International Colloquium on Automata, Languages, and Programming (ICALP 2020)

Abstract
The Strahler number of a rooted tree is the largest height of a perfect binary tree that is its minor. The Strahler number of a parity game is proposed to be defined as the smallest Strahler number of the tree of any of its attractor decompositions. It is proved that parity games can be solved in quasi-linear space and in time that is polynomial in the number of vertices n and linear in (d/(2k))^k, where d is the number of priorities and k is the Strahler number. This complexity is quasi-polynomial because the Strahler number is at most logarithmic in the number of vertices. The proof is based on a new construction of small Strahler-universal trees. It is shown that the Strahler number of a parity game is a robust, and hence arguably natural, parameter: it coincides with its alternative version based on trees of progress measures and - remarkably - with the register number defined by Lehtinen (2018). It follows that parity games can be solved in quasi-linear space and in time that is polynomial in the number of vertices and linear in (d/(2k))^k, where k is the register number. This significantly improves the running times and space achieved for parity games of bounded register number by Lehtinen (2018) and by Parys (2020). The running time of the algorithm based on small Strahler-universal trees yields a novel trade-off k ⋅ lg(d/k) = O(log n) between the two natural parameters that measure the structural complexity of a parity game, which allows solving parity games in polynomial time. This includes as special cases the asymptotic settings of those parameters covered by the results of Calude, Jain Khoussainov, Li, and Stephan (2017), of Jurdziński and Lazić (2017), and of Lehtinen (2018), and it significantly extends the range of such settings, for example to d = 2^O(√{lg n}) and k = O(√{lg n}).
Cite as

Laure Daviaud, Marcin Jurdziński, and K. S. Thejaswini. The Strahler Number of a Parity Game. In 47th International Colloquium on Automata, Languages, and Programming (ICALP 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 168, pp. 123:1-123:19, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{daviaud_et_al:LIPIcs.ICALP.2020.123,
  author =	{Daviaud, Laure and Jurdzi\'{n}ski, Marcin and Thejaswini, K. S.},
  title =	{{The Strahler Number of a Parity Game}},
  booktitle =	{47th International Colloquium on Automata, Languages, and Programming (ICALP 2020)},
  pages =	{123:1--123:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-138-2},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{168},
  editor =	{Czumaj, Artur and Dawar, Anuj and Merelli, Emanuela},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2020.123},
  URN =		{urn:nbn:de:0030-drops-125304},
  doi =		{10.4230/LIPIcs.ICALP.2020.123},
  annote =	{Keywords: parity game, attractor decomposition, progress measure, universal tree, Strahler number}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2019.36
Query Preserving Watermarking Schemes for Locally Treelike Databases

Authors: Agnishom Chattopadhyay and M. Praveen

Published in: LIPIcs, Volume 150, 39th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2019)

Abstract
Watermarking is a way of embedding information in digital documents. Much research has been done on techniques for watermarking relational databases and XML documents, where the process of embedding information shouldn't distort query outputs too much. Recently, techniques have been proposed to watermark some classes of relational structures preserving first-order and monadic second order queries. For relational structures whose Gaifman graphs have bounded degree, watermarking can be done preserving first-order queries. We extend this line of work and study watermarking schemes for other classes of structures. We prove that for relational structures whose Gaifman graphs belong to a class of graphs that have locally bounded tree-width and is closed under minors, watermarking schemes exist that preserve first-order queries. We use previously known properties of logical formulas and graphs, and build on them with some technical work to make them work in our context. This constitutes a part of the first steps to understand the extent to which techniques from algorithm design and computational learning theory can be adapted for watermarking.
Cite as

Agnishom Chattopadhyay and M. Praveen. Query Preserving Watermarking Schemes for Locally Treelike Databases. In 39th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 150, pp. 36:1-36:14, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{chattopadhyay_et_al:LIPIcs.FSTTCS.2019.36,
  author =	{Chattopadhyay, Agnishom and Praveen, M.},
  title =	{{Query Preserving Watermarking Schemes for Locally Treelike Databases}},
  booktitle =	{39th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2019)},
  pages =	{36:1--36:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-131-3},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{150},
  editor =	{Chattopadhyay, Arkadev and Gastin, Paul},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2019.36},
  URN =		{urn:nbn:de:0030-drops-115988},
  doi =		{10.4230/LIPIcs.FSTTCS.2019.36},
  annote =	{Keywords: Locally bounded tree-width, closure under minors, first-order queries, watermarking}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2018.15
Verifying Quantitative Temporal Properties of Procedural Programs

Authors: Mohamed Faouzi Atig, Ahmed Bouajjani, K. Narayan Kumar, and Prakash Saivasan

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

Abstract
We address the problem of specifying and verifying quantitative properties of procedural programs. These properties typically involve constraints on the relative cumulated costs of executing various tasks (by invoking for instance some particular procedures) within the scope of the execution of some particular procedure. An example of such properties is "within the execution of each invocation of procedure P, the time spent in executing invocations of procedure Q is less than 20 % of the total execution time". We introduce specification formalisms, both automata-based and logic-based, for expressing such properties, and we study the links between these formalisms and their application in model-checking. On one side, we define Constrained Pushdown Systems (CPDS), an extension of pushdown systems with constraints, expressed in Presburger arithmetics, on the numbers of occurrences of each symbol in the alphabet within invocation intervals (subcomputations between matching pushes and pops), and on the other side, we introduce a higher level specification language that is a quantitative extension of CaRet (the Call-Return temporal logic) called QCaRet where nested quantitative constraints over procedure invocation intervals are expressible using Presburger arithmetics. Then, we investigate (1) the decidability of the reachability and repeated reachability problems for CPDS, and (2) the effective reduction of the model-checking problem of procedural programs (modeled as visibly pushdown systems) against QCaRet formulas to these problems on CPDS.
Cite as

Mohamed Faouzi Atig, Ahmed Bouajjani, K. Narayan Kumar, and Prakash Saivasan. Verifying Quantitative Temporal Properties of Procedural Programs. In 29th International Conference on Concurrency Theory (CONCUR 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 118, pp. 15:1-15:17, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{atig_et_al:LIPIcs.CONCUR.2018.15,
  author =	{Atig, Mohamed Faouzi and Bouajjani, Ahmed and Narayan Kumar, K. and Saivasan, Prakash},
  title =	{{Verifying Quantitative Temporal Properties of Procedural Programs}},
  booktitle =	{29th International Conference on Concurrency Theory (CONCUR 2018)},
  pages =	{15:1--15:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-087-3},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{118},
  editor =	{Schewe, Sven and Zhang, Lijun},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2018.15},
  URN =		{urn:nbn:de:0030-drops-95531},
  doi =		{10.4230/LIPIcs.CONCUR.2018.15},
  annote =	{Keywords: Verification, Formal Methods, Pushdown systems, Visibly pushdown, Quantitative Temporal Properties}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2018.35
Regular Separability of Well-Structured Transition Systems

Authors: Wojciech Czerwinski, Slawomir Lasota, Roland Meyer, Sebastian Muskalla, K. Narayan Kumar, and Prakash Saivasan

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

Abstract
We investigate the languages recognized by well-structured transition systems (WSTS) with upward and downward compatibility. Our first result shows that, under very mild assumptions, every two disjoint WSTS languages are regular separable: There is a regular language containing one of them and being disjoint from the other. As a consequence, if a language as well as its complement are both recognized by WSTS, then they are necessarily regular. In particular, no subclass of WSTS languages beyond the regular languages is closed under complement. Our second result shows that for Petri nets, the complexity of the backwards coverability algorithm yields a bound on the size of the regular separator. We complement it by a lower bound construction.
Cite as

Wojciech Czerwinski, Slawomir Lasota, Roland Meyer, Sebastian Muskalla, K. Narayan Kumar, and Prakash Saivasan. Regular Separability of Well-Structured Transition Systems. In 29th International Conference on Concurrency Theory (CONCUR 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 118, pp. 35:1-35:18, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{czerwinski_et_al:LIPIcs.CONCUR.2018.35,
  author =	{Czerwinski, Wojciech and Lasota, Slawomir and Meyer, Roland and Muskalla, Sebastian and Narayan Kumar, K. and Saivasan, Prakash},
  title =	{{Regular Separability of Well-Structured Transition Systems}},
  booktitle =	{29th International Conference on Concurrency Theory (CONCUR 2018)},
  pages =	{35:1--35:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-087-3},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{118},
  editor =	{Schewe, Sven and Zhang, Lijun},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2018.35},
  URN =		{urn:nbn:de:0030-drops-95733},
  doi =		{10.4230/LIPIcs.CONCUR.2018.35},
  annote =	{Keywords: regular separability, wsts, coverability languages, Petri nets}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2017.11
Verification of Asynchronous Programs with Nested Locks

Authors: Mohamed Faouzi Atig, Ahmed Bouajjani, K. Narayan Kumar, and Prakash Saivasan

Published in: LIPIcs, Volume 93, 37th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2017)

Abstract
In this paper, we consider asynchronous programs consisting of multiple recursive threads running in parallel. Each of the threads is equipped with a multi-set. The threads can create tasks and post them onto the multi-sets or read a task from their own. In addition, they can synchronise through a finite set of locks. In this paper, we show that the reachability problem for such class of asynchronous programs is undecidable even under the nested locking policy. We then show that the reachability problem becomes decidable (Exp-space-complete) when the locks are not allowed to be held across tasks. Finally, we show that the problem is NP-complete when in addition to previous restrictions, threads always read tasks from the same state.
Cite as

Mohamed Faouzi Atig, Ahmed Bouajjani, K. Narayan Kumar, and Prakash Saivasan. Verification of Asynchronous Programs with Nested Locks. In 37th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 93, pp. 11:1-11:14, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{atig_et_al:LIPIcs.FSTTCS.2017.11,
  author =	{Atig, Mohamed Faouzi and Bouajjani, Ahmed and Narayan Kumar, K. and Saivasan, Prakash},
  title =	{{Verification of Asynchronous Programs with Nested Locks}},
  booktitle =	{37th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2017)},
  pages =	{11:1--11:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-055-2},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{93},
  editor =	{Lokam, Satya and Ramanujam, R.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2017.11},
  URN =		{urn:nbn:de:0030-drops-84106},
  doi =		{10.4230/LIPIcs.FSTTCS.2017.11},
  annote =	{Keywords: asynchronous programs locks concurrency multi-set pushdown systems, multi-threaded programs, reachability, model checking, verification, nested lockin}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2014.611
On Bounded Reachability Analysis of Shared Memory Systems

Authors: Mohamed Faouzi Atig, Ahmed Bouajjani, K. Narayan Kumar, and Prakash Saivasan

Published in: LIPIcs, Volume 29, 34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014)

Abstract
This paper addresses the reachability problem for pushdown systems communicating via shared memory. It is already known that this problem is undecidable. It turns out that undecidability holds even if the shared memory consists of a single boolean variable. We propose a restriction on the behaviours of such systems, called stage bound, towards decidability. A k stage bounded run can be split into a k stages, such that in each stage there is at most one process writing to the shared memory while any number of processes may read from it. We consider several versions of stage-bounded systems and establish decidability and complexity results.
Cite as

Mohamed Faouzi Atig, Ahmed Bouajjani, K. Narayan Kumar, and Prakash Saivasan. On Bounded Reachability Analysis of Shared Memory Systems. In 34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014). Leibniz International Proceedings in Informatics (LIPIcs), Volume 29, pp. 611-623, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2014)

Copy BibTex To Clipboard

@InProceedings{atig_et_al:LIPIcs.FSTTCS.2014.611,
  author =	{Atig, Mohamed Faouzi and Bouajjani, Ahmed and Narayan Kumar, K. and Saivasan, Prakash},
  title =	{{On Bounded Reachability Analysis of Shared Memory Systems}},
  booktitle =	{34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014)},
  pages =	{611--623},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-77-4},
  ISSN =	{1868-8969},
  year =	{2014},
  volume =	{29},
  editor =	{Raman, Venkatesh and Suresh, S. P.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2014.611},
  URN =		{urn:nbn:de:0030-drops-48754},
  doi =		{10.4230/LIPIcs.FSTTCS.2014.611},
  annote =	{Keywords: Reachability problem, Pushdown systems, Counter systems}
}
Document
Complete Volume
DOI: 10.4230/LIPIcs.FSTTCS.2009
LIPIcs, Volume 4, FSTTCS'09, Complete Volume

Authors: Ravi Kannan and K. Narayan Kumar

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

Abstract
LIPIcs, Volume 4, FSTTCS'09, Complete Volume
Cite as

Ravi Kannan and K. Narayan Kumar. LIPIcs, Volume 4, FSTTCS'09, Complete Volume. In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science. Leibniz International Proceedings in Informatics (LIPIcs), Volume 4, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2013)

Copy BibTex To Clipboard

@Proceedings{kannan_et_al:LIPIcs.FSTTCS.2009,
  title =	{{LIPIcs, Volume 4, FSTTCS'09, Complete Volume}},
  booktitle =	{IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-13-2},
  ISSN =	{1868-8969},
  year =	{2013},
  volume =	{4},
  editor =	{Kannan, Ravi and Narayan Kumar, K.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2009},
  URN =		{urn:nbn:de:0030-drops-40987},
  doi =		{10.4230/LIPIcs.FSTTCS.2009},
  annote =	{Keywords: LIPIcs, Volume 4, FSTTCS'09, Complete Volume}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2010.204
Model checking time-constrained scenario-based specifications

Authors: S. Akshay, Paul Gastin, Madhavan Mukund, and K. Narayan Kumar

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

Abstract
We consider the problem of model checking message-passing systems with real-time requirements. As behavioural specifications, we use message sequence charts (MSCs) annotated with timing constraints. Our system model is a network of communicating finite state machines with local clocks, whose global behaviour can be regarded as a timed automaton. Our goal is to verify that all timed behaviours exhibited by the system conform to the timing constraints imposed by the specification. In general, this corresponds to checking inclusion for timed languages, which is an undecidable problem even for timed regular languages. However, we show that we can translate regular collections of time-constrained MSCs into a special class of event-clock automata that can be determinized and complemented, thus permitting an algorithmic solution to the model checking problem.
Cite as

S. Akshay, Paul Gastin, Madhavan Mukund, and K. Narayan Kumar. Model checking time-constrained scenario-based specifications. In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2010). Leibniz International Proceedings in Informatics (LIPIcs), Volume 8, pp. 204-215, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2010)

Copy BibTex To Clipboard

@InProceedings{akshay_et_al:LIPIcs.FSTTCS.2010.204,
  author =	{Akshay, S. and Gastin, Paul and Mukund, Madhavan and Narayan Kumar, K.},
  title =	{{Model checking time-constrained scenario-based specifications}},
  booktitle =	{IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2010)},
  pages =	{204--215},
  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.204},
  URN =		{urn:nbn:de:0030-drops-28649},
  doi =		{10.4230/LIPIcs.FSTTCS.2010.204},
  annote =	{Keywords: model-checking, message-passing system, time-constrained MSC}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2009.2323
Verification and Refutation of Probabilistic Specifications via Games

Authors: Mark Kattenbelt and Michael Huth

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

Abstract
We develop an abstraction-based framework to check probabilistic specifications of Markov Decision Processes (MDPs) using the stochastic two-player game abstractions (\ie ``games'') developed by Kwiatkowska et al.\ as a foundation. We define an abstraction preorder for these game abstractions which enables us to identify many new game abstractions for each MDP --- ranging from compact and imprecise to complex and precise. This added ability to trade precision for efficiency is crucial for scalable software model checking, as precise abstractions are expensive to construct in practice. Furthermore, we develop a four-valued probabilistic computation tree logic (PCTL) semantics for game abstractions. Together, the preorder and PCTL semantics comprise a powerful verification and refutation framework for arbitrary PCTL properties of MDPs.
Cite as

Mark Kattenbelt and Michael Huth. Verification and Refutation of Probabilistic Specifications via Games. In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science. Leibniz International Proceedings in Informatics (LIPIcs), Volume 4, pp. 251-262, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2009)

Copy BibTex To Clipboard

@InProceedings{kattenbelt_et_al:LIPIcs.FSTTCS.2009.2323,
  author =	{Kattenbelt, Mark and Huth, Michael},
  title =	{{Verification and Refutation of Probabilistic Specifications via Games}},
  booktitle =	{IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science},
  pages =	{251--262},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-13-2},
  ISSN =	{1868-8969},
  year =	{2009},
  volume =	{4},
  editor =	{Kannan, Ravi and Narayan Kumar, K.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2009.2323},
  URN =		{urn:nbn:de:0030-drops-23233},
  doi =		{10.4230/LIPIcs.FSTTCS.2009.2323},
  annote =	{Keywords: Probabilistic model checking, Markov decision processes, Abstraction preorder, Stochastic two-player games}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2009.2324
Approximating Fault-Tolerant Group-Steiner Problems

Authors: Rohit Khandekar, Guy Kortsarz, and Zeev Nutov

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

Abstract
In this paper, we initiate the study of designing approximation algorithms for {\sf Fault-Tolerant Group-Steiner} ({\sf FTGS}) problems. The motivation is to protect the well-studied group-Steiner networks from edge or vertex failures. In {\sf Fault-Tolerant Group-Steiner} problems, we are given a graph with edge- (or vertex-) costs, a root vertex, and a collection of subsets of vertices called groups. The objective is to find a minimum-cost subgraph that has two edge- (or vertex-) disjoint paths from each group to the root. We present approximation algorithms and hardness results for several variants of this basic problem, e.g., edge-costs vs. vertex-costs, edge-connectivity vs. vertex-connectivity, and $2$-connecting from each group a single vertex vs. many vertices. Main contributions of our paper include the introduction of very general structural lemmas on connectivity and a charging scheme that may find more applications in the future. Our algorithmic results are supplemented by inapproximability results, which are tight in some cases. Our algorithms employ a variety of techniques. For the edge-connectivity variant, we use a primal-dual based algorithm for covering an {\em uncros\-sable} set-family, while for the vertex-connectivity version, we prove a new graph-theoretic lemma that shows equivalence between obtaining two vertex-disjoint paths from two vertices and $2$-connecting a carefully chosen single vertex. To handle large group-sizes, we use a $p$-Steiner tree algorithm to identify the ``correct'' pair of terminals from each group to be connected to the root. We also use a non-trivial charging scheme to improve the approximation ratio for the most general problem we consider.
Cite as

Rohit Khandekar, Guy Kortsarz, and Zeev Nutov. Approximating Fault-Tolerant Group-Steiner Problems. In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science. Leibniz International Proceedings in Informatics (LIPIcs), Volume 4, pp. 263-274, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2009)

Copy BibTex To Clipboard

@InProceedings{khandekar_et_al:LIPIcs.FSTTCS.2009.2324,
  author =	{Khandekar, Rohit and Kortsarz, Guy and Nutov, Zeev},
  title =	{{Approximating Fault-Tolerant Group-Steiner Problems}},
  booktitle =	{IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science},
  pages =	{263--274},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-13-2},
  ISSN =	{1868-8969},
  year =	{2009},
  volume =	{4},
  editor =	{Kannan, Ravi and Narayan Kumar, K.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2009.2324},
  URN =		{urn:nbn:de:0030-drops-23243},
  doi =		{10.4230/LIPIcs.FSTTCS.2009.2324},
  annote =	{Keywords: Fault-tolerance, group Steiner problem, edge-disjointness, vertex-disjointness, approximation, connectivity}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2009.2325
Bounded Size Graph Clustering with Applications to Stream Processing

Authors: Rohit Khandekar, Kirsten Hildrum, Sujay Parekh, Deepak Rajan, Jay Sethuraman, and Joel Wolf

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

Abstract
We introduce a graph clustering problem motivated by a stream processing application. Input to our problem is an undirected graph with vertex and edge weights. A cluster is a subset of the vertices. The {\em size} of a cluster is defined as the total vertex weight in the subset plus the total edge weight at the boundary of the cluster. The bounded size graph clustering problem ($\GC$) is to partition the vertices into clusters of size at most a given budget and minimize the total edge-weight across the clusters. In the {\em multiway cut} version of the problem, we are also given a subset of vertices called {\em terminals}. No cluster is allowed to contain more than one terminal. Our problem differs from most of the previously studied clustering problems in that the number of clusters is not specified. We first show that the feasibility version of the multiway cut $\GC$ problem, i.e., determining if there exists a clustering with bounded-size clusters satisfying the multiway cut constraint, can be solved in polynomial time. Our algorithm is based on the min-cut subroutine and an uncrossing argument. This result is in contrast with the NP-hardness of the min-max multiway cut problem, considered by Svitkina and Tardos (2004), in which the number of clusters must equal the number of terminals. Our results for the feasibility version also generalize to any symmetric submodular function. We next show that the optimization version of $\GC$ is NP-hard by showing an approximation-preserving reduction from the $\frac 13$-balanced cut problem. Our main result is an $O(\log^2 n)$-approximation to the optimization version of the multiway cut $\GC$ problem violating the budget by an $O(\log n)$ factor, where $n$ denotes the number of vertices. Our algorithm is based on a set-cover-like greedy approach which iteratively computes bounded-size clusters to maximize the number of new vertices covered.
Cite as

Rohit Khandekar, Kirsten Hildrum, Sujay Parekh, Deepak Rajan, Jay Sethuraman, and Joel Wolf. Bounded Size Graph Clustering with Applications to Stream Processing. In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science. Leibniz International Proceedings in Informatics (LIPIcs), Volume 4, pp. 275-286, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2009)

Copy BibTex To Clipboard

@InProceedings{khandekar_et_al:LIPIcs.FSTTCS.2009.2325,
  author =	{Khandekar, Rohit and Hildrum, Kirsten and Parekh, Sujay and Rajan, Deepak and Sethuraman, Jay and Wolf, Joel},
  title =	{{Bounded Size Graph Clustering with Applications to Stream Processing}},
  booktitle =	{IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science},
  pages =	{275--286},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-13-2},
  ISSN =	{1868-8969},
  year =	{2009},
  volume =	{4},
  editor =	{Kannan, Ravi and Narayan Kumar, K.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2009.2325},
  URN =		{urn:nbn:de:0030-drops-23250},
  doi =		{10.4230/LIPIcs.FSTTCS.2009.2325},
  annote =	{Keywords: Graph partitioning, uncrossing, Gomory-Hu trees, symmetric submodular functions}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2009.2326
A Fine-grained Analysis of a Simple Independent Set Algorithm

Authors: Joachim Kneis, Alexander Langer, and Peter Rossmanith

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

Abstract
We present a simple exact algorithm for the \is\ problem with a runtime bounded by $O(\rt^n \poly(n))$. This bound is obtained by, firstly, applying a new branching rule and, secondly, by a distinct, computer-aided case analysis. The new branching rule uses the concept of satellites and has previously only been used in an algorithm for sparse graphs. The computer-aided case analysis allows us to capture the behavior of our algorithm in more detail than in a traditional analysis. The main purpose of this paper is to demonstrate how a very simple algorithm can outperform more complicated ones if the right analysis of its running time is performed.
Cite as

Joachim Kneis, Alexander Langer, and Peter Rossmanith. A Fine-grained Analysis of a Simple Independent Set Algorithm. In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science. Leibniz International Proceedings in Informatics (LIPIcs), Volume 4, pp. 287-298, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2009)

Copy BibTex To Clipboard

@InProceedings{kneis_et_al:LIPIcs.FSTTCS.2009.2326,
  author =	{Kneis, Joachim and Langer, Alexander and Rossmanith, Peter},
  title =	{{A Fine-grained Analysis of a Simple Independent Set Algorithm}},
  booktitle =	{IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science},
  pages =	{287--298},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-13-2},
  ISSN =	{1868-8969},
  year =	{2009},
  volume =	{4},
  editor =	{Kannan, Ravi and Narayan Kumar, K.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2009.2326},
  URN =		{urn:nbn:de:0030-drops-23269},
  doi =		{10.4230/LIPIcs.FSTTCS.2009.2326},
  annote =	{Keywords: Exact Algorithms, Independent Set, Computer-aided Proof}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2009.2327
Using Elimination Theory to construct Rigid Matrices

Authors: Abhinav Kumar, Satyanarayana V. Lokam, Vijay M. Patankar, and Jayalal Sarma M. N.

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

Abstract
The rigidity of a matrix $A$ for target rank $r$ is the minimum number of entries of $A$ that must be changed to ensure that the rank of the altered matrix is at most $r$. Since its introduction by Valiant \cite{Val77}, rigidity and similar rank-robustness functions of matrices have found numerous applications in circuit complexity, communication complexity, and learning complexity. Almost all $\nbyn$ matrices over an infinite field have a rigidity of $(n-r)^2$. It is a long-standing open question to construct infinite families of \emph{explicit} matrices even with superlinear rigidity when $r=\Omega(n)$. In this paper, we construct an infinite family of complex matrices with the largest possible, i.e., $(n-r)^2$, rigidity. The entries of an $\nbyn$ matrix in this family are distinct primitive roots of unity of orders roughly \SL{$\exp(n^4 \log n)$}. To the best of our knowledge, this is the first family of concrete (but not entirely explicit) matrices having maximal rigidity and a succinct algebraic description. Our construction is based on elimination theory of polynomial ideals. In particular, we use results on the existence of polynomials in elimination ideals with effective degree upper bounds (effective Nullstellensatz). Using elementary algebraic geometry, we prove that the dimension of the affine variety of matrices of rigidity at most $k$ is exactly $n^2 - (n-r)^2 +k$. Finally, we use elimination theory to examine whether the rigidity function is semicontinuous.
Cite as

Abhinav Kumar, Satyanarayana V. Lokam, Vijay M. Patankar, and Jayalal Sarma M. N.. Using Elimination Theory to construct Rigid Matrices. In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science. Leibniz International Proceedings in Informatics (LIPIcs), Volume 4, pp. 299-310, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2009)

Copy BibTex To Clipboard

@InProceedings{kumar_et_al:LIPIcs.FSTTCS.2009.2327,
  author =	{Kumar, Abhinav and Lokam, Satyanarayana V. and Patankar, Vijay M. and Sarma M. N., Jayalal},
  title =	{{Using Elimination Theory to construct Rigid Matrices}},
  booktitle =	{IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science},
  pages =	{299--310},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-13-2},
  ISSN =	{1868-8969},
  year =	{2009},
  volume =	{4},
  editor =	{Kannan, Ravi and Narayan Kumar, K.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2009.2327},
  URN =		{urn:nbn:de:0030-drops-23278},
  doi =		{10.4230/LIPIcs.FSTTCS.2009.2327},
  annote =	{Keywords: Matrix Rigidity, Lower Bounds, Circuit Complexity}
}
  • Refine by Author
  • 7 Narayan Kumar, K.
  • 4 Saivasan, Prakash
  • 3 Atig, Mohamed Faouzi
  • 3 Bouajjani, Ahmed
  • 3 Praveen, M.
  • Show More...

  • Refine by Classification
  • 2 Theory of computation → Formal languages and automata theory
  • 2 Theory of computation → Logic and verification
  • 1 Information systems → Relational database model
  • 1 Security and privacy → Information accountability and usage control
  • 1 Software and its engineering → Model checking
  • Show More...

  • Refine by Keyword
  • 3 Petri nets
  • 2 Buchi Automata
  • 2 Pushdown systems
  • 2 model-checking
  • 2 monadic second-order logic
  • Show More...

  • Refine by Type
  • 49 document
  • 1 volume

  • Refine by Publication Year
  • 41 2009
  • 3 2018
  • 2 2020
  • 1 2010
  • 1 2013
  • 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 Schloss Dagstuhl - LZI GmbH Imprint Privacy Contact