62 Search Results for "D'Souza, Deepak"

Volume

LIPIcs, Volume 18

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

FSTTCS 2012, December 15-17, 2012, Hyderabad, India

Editors: Deepak D'Souza, Jaikumar Radhakrishnan, and Kavitha Telikepalli

Document
DOI: 10.4230/LIPIcs.STACS.2026.64
One-Clock Synthesis Problems

Authors: Sławomir Lasota, Mathieu Lehaut, Julie Parreaux, and Radosław Piórkowski

Published in: LIPIcs, Volume 364, 43rd International Symposium on Theoretical Aspects of Computer Science (STACS 2026)

Abstract
We study a generalisation of Büchi-Landweber games to the timed setting. The winning condition is specified by a non-deterministic timed automaton, and one of the players can elapse time. We perform a systematic study of synthesis problems in all variants of timed games, depending on which player’s winning condition is specified, and which player’s strategy (or controller, a finite-memory strategy) is sought. As our main result we prove ubiquitous undecidability in all the variants, both for strategy and controller synthesis, already for winning conditions specified by one-clock automata. This strengthens and generalises previously known undecidability results. We also fully characterise those cases where finite memory is sufficient to win, namely existence of a strategy implies existence of a controller. All our results are stated in the timed setting, while analogous results hold in the data setting where one-clock automata are replaced by one-register ones.
Cite as

Sławomir Lasota, Mathieu Lehaut, Julie Parreaux, and Radosław Piórkowski. One-Clock Synthesis Problems. In 43rd International Symposium on Theoretical Aspects of Computer Science (STACS 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 364, pp. 64:1-64:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{lasota_et_al:LIPIcs.STACS.2026.64,
  author =	{Lasota, S{\l}awomir and Lehaut, Mathieu and Parreaux, Julie and Pi\'{o}rkowski, Rados{\l}aw},
  title =	{{One-Clock Synthesis Problems}},
  booktitle =	{43rd International Symposium on Theoretical Aspects of Computer Science (STACS 2026)},
  pages =	{64:1--64:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-412-3},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{364},
  editor =	{Mahajan, Meena and Manea, Florin and McIver, Annabelle and Thắng, Nguy\~{ê}n Kim},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2026.64},
  URN =		{urn:nbn:de:0030-drops-255533},
  doi =		{10.4230/LIPIcs.STACS.2026.64},
  annote =	{Keywords: timed automata, register automata, B\"{u}chi-Landweber games, Church synthesis problem, reactive synthesis problem}
}
Document
DOI: 10.4230/LIPIcs.CSL.2026.8
Register-Bounded Synthesis from Constraint LTL

Authors: Nino Dauvier, Emmanuel Filiot, and Pierre-Alain Reynier

Published in: LIPIcs, Volume 363, 34th EACSL Annual Conference on Computer Science Logic (CSL 2026)

Abstract
We consider synthesis problems from logical specifications over infinite data domains, expressed in the logic constraint LTL (CLTL), which extends LTL with predicates over an infinite set of data values. We consider register-bounded synthesis, where the goal is to automatically generate, if it exists, a transducer with r registers that realizes a given CLTL formula, where r is also given as input. We prove that CLTL register-bounded synthesis is 2ExpTime-c for various data domains such as any infinite set with equality, (ℚ, <), and (ℕ, <). For the latter domain, this contrasts with known undecidability results of (unbounded) register CLTL synthesis, by Bhaskar and Praveen. Lastly, we consider synthesis in a partial observation setting by extending CLTL with invisible variables.
Cite as

Nino Dauvier, Emmanuel Filiot, and Pierre-Alain Reynier. Register-Bounded Synthesis from Constraint LTL. In 34th EACSL Annual Conference on Computer Science Logic (CSL 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 363, pp. 8:1-8:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{dauvier_et_al:LIPIcs.CSL.2026.8,
  author =	{Dauvier, Nino and Filiot, Emmanuel and Reynier, Pierre-Alain},
  title =	{{Register-Bounded Synthesis from Constraint LTL}},
  booktitle =	{34th EACSL Annual Conference on Computer Science Logic (CSL 2026)},
  pages =	{8:1--8:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-411-6},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{363},
  editor =	{Guerrini, Stefano and K\"{o}nig, Barbara},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2026.8},
  URN =		{urn:nbn:de:0030-drops-254322},
  doi =		{10.4230/LIPIcs.CSL.2026.8},
  annote =	{Keywords: Synthesis, Data words, Constraint linear time logic, Register transducer}
}
Document
DOI: 10.4230/LIPIcs.CSL.2026.31
Parametric Disjunctive Timed Networks

Authors: Étienne André, Swen Jacobs, and Engel Lefaucheux

Published in: LIPIcs, Volume 363, 34th EACSL Annual Conference on Computer Science Logic (CSL 2026)

Abstract
We consider distributed systems with an arbitrary number of processes, modelled by timed automata that communicate through location guards: a process can take a guarded transition if at least one other process is in a given location. In this work, we introduce parametric disjunctive timed networks, where each timed automaton may contain timing parameters, i.e., unknown constants. We investigate two problems: deciding the emptiness of the set of parameter valuations for which 1) a given location is reachable for at least one process (local property), and 2) a global state is reachable where all processes are in a given location (global property). Our main positive result is that the first problem is decidable for networks of processes with a single clock and without invariants; this result holds for arbitrarily many timing parameters - a setting with few known decidability results. However, it becomes undecidable when invariants are allowed, or when considering global properties, even for systems with a single parameter. This highlights the significant expressive power of invariants in these networks. Additionally, we exhibit further decidable subclasses by restraining the syntax of guards and invariants.
Cite as

Étienne André, Swen Jacobs, and Engel Lefaucheux. Parametric Disjunctive Timed Networks. In 34th EACSL Annual Conference on Computer Science Logic (CSL 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 363, pp. 31:1-31:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{andre_et_al:LIPIcs.CSL.2026.31,
  author =	{Andr\'{e}, \'{E}tienne and Jacobs, Swen and Lefaucheux, Engel},
  title =	{{Parametric Disjunctive Timed Networks}},
  booktitle =	{34th EACSL Annual Conference on Computer Science Logic (CSL 2026)},
  pages =	{31:1--31:24},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-411-6},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{363},
  editor =	{Guerrini, Stefano and K\"{o}nig, Barbara},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2026.31},
  URN =		{urn:nbn:de:0030-drops-254562},
  doi =		{10.4230/LIPIcs.CSL.2026.31},
  annote =	{Keywords: parametrised verification, parametric timed automata, verification of infinite-state systems}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2025.8
Parameterized Verification of Timed Networks with Clock Invariants

Authors: Étienne André, Swen Jacobs, Shyam Lal Karra, and Ocan Sankur

Published in: LIPIcs, Volume 360, 45th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2025)

Abstract
We consider parameterized verification problems for networks of timed automata (TAs) based on different communication primitives. To this end, we first consider disjunctive timed networks (DTNs), i.e., networks of TAs that communicate via location guards that enable a transition only if there is another process in a certain location. We solve for the first time the case with unrestricted clock invariants, and establish that the parameterized model checking problem (PMCP) over finite local traces can be reduced to the corresponding model checking problem on a single TA. Moreover, we prove that the PMCP for networks that communicate via lossy broadcast can be reduced to the PMCP for DTNs. Finally, we show that for networks with k-wise synchronization, and therefore also for timed Petri nets, location reachability can be reduced to location reachability in DTNs. As a consequence we can answer positively the open problem from Abdulla et al. (2018) whether the universal safety problem for timed Petri nets with multiple clocks is decidable.
Cite as

Étienne André, Swen Jacobs, Shyam Lal Karra, and Ocan Sankur. Parameterized Verification of Timed Networks with Clock Invariants. In 45th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 360, pp. 8:1-8:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{andre_et_al:LIPIcs.FSTTCS.2025.8,
  author =	{Andr\'{e}, \'{E}tienne and Jacobs, Swen and Karra, Shyam Lal and Sankur, Ocan},
  title =	{{Parameterized Verification of Timed Networks with Clock Invariants}},
  booktitle =	{45th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2025)},
  pages =	{8:1--8:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-406-2},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{360},
  editor =	{Aiswarya, C. and Mehta, Ruta and Roy, Subhajit},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2025.8},
  URN =		{urn:nbn:de:0030-drops-250878},
  doi =		{10.4230/LIPIcs.FSTTCS.2025.8},
  annote =	{Keywords: Networks of Timed Automata, Parameterized Verification, Timed Petri Nets}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2025.14
Regulating Synchronous Data Exchange to Meet Control Flow and Data Specifications

Authors: Ashwin Bhaskar and M. Praveen

Published in: LIPIcs, Volume 360, 45th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2025)

Abstract
When multiple software components interact via method calls, we may want to ensure that the order of invoked methods and the arguments provided adhere to some specification. The classic problem associated with interface automata checks for the existence of a mediator whose intention is to act as a buffer in between method invocations so that invocations do not go unanswered. We extend the base model underlying interface automata, enabling them to exchange integer values - one automaton generates an integer value and outputs it by firing a generating transition and another automaton receives the value by synchronously firing a receiving transition. Transitions in the automata can have guards with linear order constraints on the exchanged values, influencing which methods can or can not be invoked later. So the generated values influence the sequences of invocations that are enabled. We specify desirable properties of the sequence of method calls and the arguments passed to them using an extension of Linear Temporal Logic (LTL). We consider the interoperability problem, which is to check if it is possible to generate integer values in such a way that all enabled sequences satisfy the given specification. We show that the interoperability problem is undecidable in general, even when there are only two participating automata. We show decidability in the case where guards on generating transitions can only have equality constraints on the exchanged value (but receiving transitions can continue to have linear order constraints). We model this problem as a game between two players, one trying to generate integer values such that violating sequences are disabled while the other player tries to dig out violating sequences that are enabled. Interoperability is equivalent to the first player having a winning strategy. We solve this game via a finite abstraction, which results in a symbolic game. We then show that winning strategies for the symbolic game can be translated to winning strategies for the original game over integers.
Cite as

Ashwin Bhaskar and M. Praveen. Regulating Synchronous Data Exchange to Meet Control Flow and Data Specifications. In 45th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 360, pp. 14:1-14:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{bhaskar_et_al:LIPIcs.FSTTCS.2025.14,
  author =	{Bhaskar, Ashwin and Praveen, M.},
  title =	{{Regulating Synchronous Data Exchange to Meet Control Flow and Data Specifications}},
  booktitle =	{45th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2025)},
  pages =	{14:1--14:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-406-2},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{360},
  editor =	{Aiswarya, C. and Mehta, Ruta and Roy, Subhajit},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2025.14},
  URN =		{urn:nbn:de:0030-drops-250962},
  doi =		{10.4230/LIPIcs.FSTTCS.2025.14},
  annote =	{Keywords: Distributed Systems, Interface Automata, Registers, Parity Games}
}
Document
DOI: 10.4230/LIPIcs.ECOOP.2025.34
Taming and Dissecting Recursions Through Interprocedural Weak Topological Ordering

Authors: Jiawei Yang, Xiao Cheng, Bor-Yuh Evan Chang, Xiapu Luo, and Yulei Sui

Published in: LIPIcs, Volume 333, 39th European Conference on Object-Oriented Programming (ECOOP 2025)

Abstract
Abstract interpretation provides a foundational framework for approximating program semantics by interpreting code through abstract domains using semantic functions over ordered sets along a program’s control flow graph (CFG). To facilitate fixpoint computation in abstract interpretation, weak topological ordering (WTO) is an effective strategy for handling loops, as it identifies strategic control points in the CFG where widening and narrowing operations should be applied. However, existing abstract interpreters still face challenges when extending WTO computation in the presence of recursive programs. Computing a precise whole-program WTO requires full context-sensitive analysis which is not scalable for large programs, while context-insensitive analysis introduces spurious cycles that compromise precision. Current approaches either ignore recursion (resulting in unsoundness) or rely on conservative approximations, sacrificing precision by adopting the greatest elements of abstract domains and applying widening at function boundaries without subsequent narrowing refinements. These can lead to undesired results for downstream tasks, such as bug detection. To address the above limitations, we present RecTopo, a new technique to boost the efficiency of precise abstract interpretation in the presence of recursive programs through interprocedural weak topological ordering (IWTO). Rather than pursuing an expensive whole-program WTO analysis, RecTopo employs an on-demand approach that strategically decomposes programs at recursion boundaries and constructs targeted IWTOs for each recursive component. RecTopo dissects and analyzes (nested) recursions through interleaved widening and narrowing operations. This approach enables precise control over interpretation ordering within recursive structures while eliminating spurious recursions through systematic correlation of control flow and call graphs. We implemented RecTopo and evaluated its effectiveness using an assertion-based checking client focused on buffer overflow detection, comparing it against three popular open-source abstract interpreters (IKOS, Clam, CSA). The experiments on 8312 programs from the NIST dataset demonstrate that, on average, RecTopo is 31.99% more precise and achieves a 17.49% higher recall rate compared to three other tools. Moreover, RecTopo exhibits an average precision improvement of 46.51% and a higher recall rate of 32.98% compared to our baselines across ten large open-source projects. Further ablation studies reveal that IWTO reduces spurious widening operations compared to whole-program WTO, resulting in a 12.83% reduction in analysis time.
Cite as

Jiawei Yang, Xiao Cheng, Bor-Yuh Evan Chang, Xiapu Luo, and Yulei Sui. Taming and Dissecting Recursions Through Interprocedural Weak Topological Ordering. In 39th European Conference on Object-Oriented Programming (ECOOP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 333, pp. 34:1-34:31, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{yang_et_al:LIPIcs.ECOOP.2025.34,
  author =	{Yang, Jiawei and Cheng, Xiao and Chang, Bor-Yuh Evan and Luo, Xiapu and Sui, Yulei},
  title =	{{Taming and Dissecting Recursions Through Interprocedural Weak Topological Ordering}},
  booktitle =	{39th European Conference on Object-Oriented Programming (ECOOP 2025)},
  pages =	{34:1--34:31},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-373-7},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{333},
  editor =	{Aldrich, Jonathan and Silva, Alexandra},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2025.34},
  URN =		{urn:nbn:de:0030-drops-233265},
  doi =		{10.4230/LIPIcs.ECOOP.2025.34},
  annote =	{Keywords: Abstract interpretation, recursion, weak topological ordering}
}
Document
DOI: 10.4230/LIPIcs.ECOOP.2025.36
Efficient Neural Network Verification via Order Leading Exploration of Branch-and-Bound Trees

Authors: Guanqin Zhang, Kota Fukuda, Zhenya Zhang, H.M.N. Dilum Bandara, Shiping Chen, Jianjun Zhao, and Yulei Sui

Published in: LIPIcs, Volume 333, 39th European Conference on Object-Oriented Programming (ECOOP 2025)

Abstract
The vulnerability of neural networks to adversarial perturbations has necessitated formal verification techniques that can rigorously certify the quality of neural networks. As the state-of-the-art, branch-and-bound (BaB) is a "divide-and-conquer" strategy that applies off-the-shelf verifiers to sub-problems for which they perform better. While BaB can identify the sub-problems that are necessary to be split, it explores the space of these sub-problems in a naive "first-come-first-served" manner, thereby suffering from an issue of inefficiency to reach a verification conclusion. To bridge this gap, we introduce an order over different sub-problems produced by BaB, concerning with their different likelihoods of containing counterexamples. Based on this order, we propose a novel verification framework Oliva that explores the sub-problem space by prioritizing those sub-problems that are more likely to find counterexamples, in order to efficiently reach the conclusion of the verification. Even if no counterexample can be found in any sub-problem, it only changes the order of visiting different sub-problems and so will not lead to a performance degradation. Specifically, Oliva has two variants, including Oliva^GR, a greedy strategy that always prioritizes the sub-problems that are more likely to find counterexamples, and Oliva^SA, a balanced strategy inspired by simulated annealing that gradually shifts from exploration to exploitation to locate the globally optimal sub-problems. We experimentally evaluate the performance of Oliva on 690 verification problems spanning over 5 models with datasets MNIST and CIFAR-10. Compared to the state-of-the-art approaches, we demonstrate the speedup of Oliva for up to 25× in MNIST, and up to 80× in CIFAR-10.
Cite as

Guanqin Zhang, Kota Fukuda, Zhenya Zhang, H.M.N. Dilum Bandara, Shiping Chen, Jianjun Zhao, and Yulei Sui. Efficient Neural Network Verification via Order Leading Exploration of Branch-and-Bound Trees. In 39th European Conference on Object-Oriented Programming (ECOOP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 333, pp. 36:1-36:29, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{zhang_et_al:LIPIcs.ECOOP.2025.36,
  author =	{Zhang, Guanqin and Fukuda, Kota and Zhang, Zhenya and Bandara, H.M.N. Dilum and Chen, Shiping and Zhao, Jianjun and Sui, Yulei},
  title =	{{Efficient Neural Network Verification via Order Leading Exploration of Branch-and-Bound Trees}},
  booktitle =	{39th European Conference on Object-Oriented Programming (ECOOP 2025)},
  pages =	{36:1--36:29},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-373-7},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{333},
  editor =	{Aldrich, Jonathan and Silva, Alexandra},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2025.36},
  URN =		{urn:nbn:de:0030-drops-233281},
  doi =		{10.4230/LIPIcs.ECOOP.2025.36},
  annote =	{Keywords: neural network verification, branch and bound, counterexample potentiality, simulated annealing, stochastic optimization}
}
Document
DOI: 10.4230/LIPIcs.ICDT.2025.4
Learning Aggregate Queries Defined by First-Order Logic with Counting

Authors: Steffen van Bergerem and Nicole Schweikardt

Published in: LIPIcs, Volume 328, 28th International Conference on Database Theory (ICDT 2025)

Abstract
In the logical framework introduced by Grohe and Turán (TOCS 2004) for Boolean classification problems, the instances to classify are tuples from a logical structure, and Boolean classifiers are described by parametric models based on logical formulas. This is a specific scenario for supervised passive learning, where classifiers should be learned based on labelled examples. Existing results in this scenario focus on Boolean classification. This paper presents learnability results beyond Boolean classification. We focus on multiclass classification problems where the task is to assign input tuples to arbitrary integers. To represent such integer-valued classifiers, we use aggregate queries specified by an extension of first-order logic with counting terms called FOC₁. Our main result shows the following: given a database of polylogarithmic degree, within quasi-linear time, we can build an index structure that makes it possible to learn FOC₁-definable integer-valued classifiers in time polylogarithmic in the size of the database and polynomial in the number of training examples.
Cite as

Steffen van Bergerem and Nicole Schweikardt. Learning Aggregate Queries Defined by First-Order Logic with Counting. In 28th International Conference on Database Theory (ICDT 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 328, pp. 4:1-4:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{vanbergerem_et_al:LIPIcs.ICDT.2025.4,
  author =	{van Bergerem, Steffen and Schweikardt, Nicole},
  title =	{{Learning Aggregate Queries Defined by First-Order Logic with Counting}},
  booktitle =	{28th International Conference on Database Theory (ICDT 2025)},
  pages =	{4:1--4:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-364-5},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{328},
  editor =	{Roy, Sudeepa and Kara, Ahmet},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICDT.2025.4},
  URN =		{urn:nbn:de:0030-drops-229457},
  doi =		{10.4230/LIPIcs.ICDT.2025.4},
  annote =	{Keywords: Supervised learning, multiclass classification problems, counting logic}
}
Document
DOI: 10.4230/LIPIcs.CSL.2025.8
The Parameterized Complexity of Learning Monadic Second-Order Logic

Authors: Steffen van Bergerem, Martin Grohe, and Nina Runde

Published in: LIPIcs, Volume 326, 33rd EACSL Annual Conference on Computer Science Logic (CSL 2025)

Abstract
Within the model-theoretic framework for supervised learning introduced by Grohe and Turán (TOCS 2004), we study the parameterized complexity of learning concepts definable in monadic second-order logic (MSO). We show that the problem of learning an MSO-definable concept from a training sequence of labeled examples is fixed-parameter tractable on graphs of bounded clique-width, and that it is hard for the parameterized complexity class para-NP on general graphs. It turns out that an important distinction to be made is between 1-dimensional and higher-dimensional concepts, where the instances of a k-dimensional concept are k-tuples of vertices of a graph. For the higher-dimensional case, we give a learning algorithm that is fixed-parameter tractable in the size of the graph, but not in the size of the training sequence, and we give a hardness result showing that this is optimal. By comparison, in the 1-dimensional case, we obtain an algorithm that is fixed-parameter tractable in both.
Cite as

Steffen van Bergerem, Martin Grohe, and Nina Runde. The Parameterized Complexity of Learning Monadic Second-Order Logic. In 33rd EACSL Annual Conference on Computer Science Logic (CSL 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 326, pp. 8:1-8:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{vanbergerem_et_al:LIPIcs.CSL.2025.8,
  author =	{van Bergerem, Steffen and Grohe, Martin and Runde, Nina},
  title =	{{The Parameterized Complexity of Learning Monadic Second-Order Logic}},
  booktitle =	{33rd EACSL Annual Conference on Computer Science Logic (CSL 2025)},
  pages =	{8:1--8:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-362-1},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{326},
  editor =	{Endrullis, J\"{o}rg and Schmitz, Sylvain},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2025.8},
  URN =		{urn:nbn:de:0030-drops-227651},
  doi =		{10.4230/LIPIcs.CSL.2025.8},
  annote =	{Keywords: monadic second-order definable concept learning, agnostic probably approximately correct learning, parameterized complexity, clique-width, fixed-parameter tractable, Boolean classification, supervised learning, monadic second-order logic}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2021.45
On the Expressive Equivalence of TPTL in the Pointwise and Continuous Semantics

Authors: Raveendra Holla, Nabarun Deka, and Deepak D'Souza

Published in: LIPIcs, Volume 213, 41st IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2021)

Abstract
We consider a first-order logic with linear constraints interpreted in a pointwise and continuous manner over timed words. We show that the two interpretations of this logic coincide in terms of expressiveness, via an effective transformation of sentences from one logic to the other. As a consequence it follows that the pointwise and continuous semantics of the logic TPTL with the since operator also coincide. Along the way we exhibit a useful normal form for sentences in these logics.
Cite as

Raveendra Holla, Nabarun Deka, and Deepak D'Souza. On the Expressive Equivalence of TPTL in the Pointwise and Continuous Semantics. In 41st IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 213, pp. 45:1-45:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{holla_et_al:LIPIcs.FSTTCS.2021.45,
  author =	{Holla, Raveendra and Deka, Nabarun and D'Souza, Deepak},
  title =	{{On the Expressive Equivalence of TPTL in the Pointwise and Continuous Semantics}},
  booktitle =	{41st IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2021)},
  pages =	{45:1--45:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-215-0},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{213},
  editor =	{Boja\'{n}czyk, Miko{\l}aj and Chekuri, Chandra},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2021.45},
  URN =		{urn:nbn:de:0030-drops-155562},
  doi =		{10.4230/LIPIcs.FSTTCS.2021.45},
  annote =	{Keywords: Real-Time Logics, First-Order Logics}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2020.57
Static Race Detection for RTOS Applications

Authors: Rishi Tulsyan, Rekha Pai, and Deepak D'Souza

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

Abstract
We present a static analysis technique for detecting data races in Real-Time Operating System (RTOS) applications. These applications are often employed in safety-critical tasks and the presence of races may lead to erroneous behaviour with serious consequences. Analyzing these applications is challenging due to the variety of non-standard synchronization mechanisms they use. We propose a technique based on the notion of an "occurs-in-between" relation between statements. This notion enables us to capture the interplay of various synchronization mechanisms. We use a pre-analysis and a small set of not-occurs-in-between patterns to detect whether two statements may race with each other. Our experimental evaluation shows that the technique is efficient and effective in identifying races with high precision.
Cite as

Rishi Tulsyan, Rekha Pai, and Deepak D'Souza. Static Race Detection for RTOS Applications. 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. 57:1-57:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{tulsyan_et_al:LIPIcs.FSTTCS.2020.57,
  author =	{Tulsyan, Rishi and Pai, Rekha and D'Souza, Deepak},
  title =	{{Static Race Detection for RTOS Applications}},
  booktitle =	{40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2020)},
  pages =	{57:1--57:20},
  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.57},
  URN =		{urn:nbn:de:0030-drops-132983},
  doi =		{10.4230/LIPIcs.FSTTCS.2020.57},
  annote =	{Keywords: Static analysis, concurrency, data-race detection, RTOS}
}
Document
Complete Volume
DOI: 10.4230/LIPIcs.FSTTCS.2012
LIPIcs, Volume 18, FSTTCS'12, Complete Volume

Authors: Deepak D'Souza, Telikepalli Kavitha, and Jaikumar Radhakrishnan

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

Abstract
LIPIcs, Volume 18, FSTTCS'12, Complete Volume
Cite as

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

Copy BibTex To Clipboard

@Proceedings{dsouza_et_al:LIPIcs.FSTTCS.2012,
  title =	{{LIPIcs, Volume 18, FSTTCS'12, Complete Volume}},
  booktitle =	{IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2012)},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-47-7},
  ISSN =	{1868-8969},
  year =	{2013},
  volume =	{18},
  editor =	{D'Souza, Deepak and Radhakrishnan, Jaikumar and Telikepalli, Kavitha},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2012},
  URN =		{urn:nbn:de:0030-drops-41121},
  doi =		{10.4230/LIPIcs.FSTTCS.2012},
  annote =	{Keywords: Software/Program Verification, Models of Computation, Modes of Computation, Complexity Measures and Classes, Nonnumerical Algorithms and Problems Specifying and Verifying and Reasoning about Programs, Mathematical Logic, Formal Languages}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2012.224
Safety Verification of Communicating One-Counter Machines

Authors: Alexander Heußner, Tristan Le Gall, and Grégoire Sutre

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

Abstract
In order to verify protocols that tag messages with integer values, we investigate the decidability of the reachability problem for systems of communicating one-counter machines. These systems consist of local one-counter machines that asynchronously communicate by exchanging the value of their counters via, a priori unbounded, FIFO channels. This model extends communicating finite-state machines (CFSM) by infinite-state local processes and an infinite message alphabet. The main result of the paper is a complete characterization of the communication topologies that have a solvable reachability question. As already CFSM exclude the possibility of automatic verification in presence of mutual communication, we also consider an under-approximative approach to the reachability problem, based on rendezvous synchronization.
Cite as

Alexander Heußner, Tristan Le Gall, and Grégoire Sutre. Safety Verification of Communicating One-Counter Machines. In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2012). Leibniz International Proceedings in Informatics (LIPIcs), Volume 18, pp. 224-235, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2012)

Copy BibTex To Clipboard

@InProceedings{heuner_et_al:LIPIcs.FSTTCS.2012.224,
  author =	{Heu{\ss}ner, Alexander and Le Gall, Tristan and Sutre, Gr\'{e}goire},
  title =	{{Safety Verification of Communicating One-Counter Machines}},
  booktitle =	{IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2012)},
  pages =	{224--235},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-47-7},
  ISSN =	{1868-8969},
  year =	{2012},
  volume =	{18},
  editor =	{D'Souza, Deepak and Radhakrishnan, Jaikumar and Telikepalli, Kavitha},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2012.224},
  URN =		{urn:nbn:de:0030-drops-38614},
  doi =		{10.4230/LIPIcs.FSTTCS.2012.224},
  annote =	{Keywords: Counter Machines, FIFO Channels, Reachability Problem, Data Words}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2012.236
Density Functions subject to a Co-Matroid Constraint

Authors: Venkatesan T. Chakaravarthy, Natwar Modani, Sivaramakrishnan R. Natarajan, Sambuddha Roy, and Yogish Sabharwal

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

Abstract
In this paper we consider the problem of finding the densest subset subject to co-matroid constraints. We are given a monotone supermodular set function f defined over a universe U, and the density of a subset S is defined to be f(S)/|S|. This generalizes the concept of graph density. Co-matroid constraints are the following: given matroid M a set S is feasible, iff the complement of S is independent in the matroid. Under such constraints, the problem becomes NP-hard. The specific case of graph density has been considered in literature under specific co-matroid constraints, for example, the cardinality matroid and the partition matroid. We show a 2-approximation for finding the densest subset subject to co-matroid constraints. Thereby we improve the approximation guarantees for the result for partition matroids in the literature.
Cite as

Venkatesan T. Chakaravarthy, Natwar Modani, Sivaramakrishnan R. Natarajan, Sambuddha Roy, and Yogish Sabharwal. Density Functions subject to a Co-Matroid Constraint. In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2012). Leibniz International Proceedings in Informatics (LIPIcs), Volume 18, pp. 236-248, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2012)

Copy BibTex To Clipboard

@InProceedings{chakaravarthy_et_al:LIPIcs.FSTTCS.2012.236,
  author =	{Chakaravarthy, Venkatesan T. and Modani, Natwar and Natarajan, Sivaramakrishnan R. and Roy, Sambuddha and Sabharwal, Yogish},
  title =	{{Density Functions subject to a Co-Matroid Constraint}},
  booktitle =	{IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2012)},
  pages =	{236--248},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-47-7},
  ISSN =	{1868-8969},
  year =	{2012},
  volume =	{18},
  editor =	{D'Souza, Deepak and Radhakrishnan, Jaikumar and Telikepalli, Kavitha},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2012.236},
  URN =		{urn:nbn:de:0030-drops-38627},
  doi =		{10.4230/LIPIcs.FSTTCS.2012.236},
  annote =	{Keywords: Approximation Algorithms, Submodular Functions, Graph Density}
}
  • Refine by Type
  • 61 Document/PDF
  • 9 Document/HTML
  • 1 Volume

  • Refine by Publication Year
  • 3 2026
  • 6 2025
  • 1 2021
  • 1 2020
  • 1 2013
  • Show More...

  • Refine by Author
  • 4 D'Souza, Deepak
  • 2 André, Étienne
  • 2 Bojanczyk, Mikolaj
  • 2 Chakaravarthy, Venkatesan T.
  • 2 Hermanns, Holger
  • Show More...

  • Refine by Series/Journal
  • 61 LIPIcs

  • Refine by Classification
  • 3 Theory of computation → Modal and temporal logics
  • 2 Computing methodologies → Logical and relational learning
  • 2 Computing methodologies → Supervised learning
  • 2 Software and its engineering → Formal software verification
  • 2 Theory of computation → Automata over infinite objects
  • Show More...

  • Refine by Keyword
  • 3 Approximation Algorithms
  • 2 Parameterized Verification
  • 2 Parity Games
  • 2 Scheduling
  • 2 concurrency
  • Show More...

Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2026 Schloss Dagstuhl – LZI GmbH Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact