6 Search Results for "Fages, François"

Document
DOI: 10.4230/LIPIcs.CP.2025.17
Scalable Counting of Minimal Trap Spaces and Fixed Points in Boolean Networks

Authors: Mohimenul Kabir, Van-Giang Trinh, Samuel Pastva, and Kuldeep S Meel

Published in: LIPIcs, Volume 340, 31st International Conference on Principles and Practice of Constraint Programming (CP 2025)

Abstract
Boolean Networks (BNs) serve as a fundamental modeling framework for capturing complex dynamical systems across various domains, including systems biology, computational logic, and artificial intelligence. A crucial property of BNs is the presence of trap spaces - subspaces of the state space that, once entered, cannot be exited. Minimal trap spaces, in particular, play a significant role in analyzing the long-term behavior of BNs, making their efficient enumeration and counting essential. The fixed points in BNs are a special case of minimal trap spaces. In this work, we formulate several meaningful counting problems related to minimal trap spaces and fixed points in BNs. These problems provide valuable insights both within BN theory (e.g., in probabilistic reasoning and dynamical analysis) and in broader application areas, including systems biology, abstract argumentation, and logic programming. To address these computational challenges, we propose novel methods based on approximate answer set counting, leveraging techniques from answer set programming. Our approach efficiently approximates the number of minimal trap spaces and the number of fixed points without requiring exhaustive enumeration, making it particularly well-suited for large-scale BNs. Our experimental evaluation on an extensive and diverse set of benchmark instances shows that our methods significantly improve the feasibility of counting minimal trap spaces and fixed points, paving the way for new applications in BN analysis and beyond.
Cite as

Mohimenul Kabir, Van-Giang Trinh, Samuel Pastva, and Kuldeep S Meel. Scalable Counting of Minimal Trap Spaces and Fixed Points in Boolean Networks. In 31st International Conference on Principles and Practice of Constraint Programming (CP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 340, pp. 17:1-17:26, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{kabir_et_al:LIPIcs.CP.2025.17,
  author =	{Kabir, Mohimenul and Trinh, Van-Giang and Pastva, Samuel and Meel, Kuldeep S},
  title =	{{Scalable Counting of Minimal Trap Spaces and Fixed Points in Boolean Networks}},
  booktitle =	{31st International Conference on Principles and Practice of Constraint Programming (CP 2025)},
  pages =	{17:1--17:26},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-380-5},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{340},
  editor =	{de la Banda, Maria Garcia},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2025.17},
  URN =		{urn:nbn:de:0030-drops-238780},
  doi =		{10.4230/LIPIcs.CP.2025.17},
  annote =	{Keywords: Computational systems biology, Boolean network, Fixed point, Trap space, Answer set counting, Projected counting, Abstract argumentation, Logic programming}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2025.8
The Unification Type of an Equational Theory May Depend on the Instantiation Preorder

Authors: Franz Baader and Oliver Fernández Gil

Published in: LIPIcs, Volume 337, 10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025)

Abstract
The unification type of an equational theory is defined using a preorder on substitutions, called the instantiation preorder, whose scope is either restricted to the variables occurring in the unification problem, or unrestricted such that all variables are considered. It has been known for more than three decades that the unification type of an equational theory may vary, depending on which instantiation preorder is used. More precisely, it was shown in 1991 that the theory ACUI of an associative, commutative, and idempotent binary function symbol with a unit is unitary w.r.t. the restricted instantiation preorder, but not unitary w.r.t. the unrestricted one. In 2016 this result was strengthened by showing that the unrestricted type of this theory also cannot be finitary. Here, we considerably improve on this result by proving that ACUI is infinitary w.r.t. the unrestricted instantiation preorder, thus precluding type zero. We also show that, w.r.t. this preorder, the unification type of ACU (where idempotency is removed from the axioms) and of AC (where additionally the unit is removed) is infinitary, though it is respectively unitary and finitary in the restricted case. In the other direction, we prove (using the example of unification in the description logic EL) that the unification type may actually improve from type zero to infinitary when switching from the restricted instantiation preorder to the unrestricted one. In addition, we establish some general results on the relationship between the two instantiation preorders.
Cite as

Franz Baader and Oliver Fernández Gil. The Unification Type of an Equational Theory May Depend on the Instantiation Preorder. In 10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 337, pp. 8:1-8:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{baader_et_al:LIPIcs.FSCD.2025.8,
  author =	{Baader, Franz and Fern\'{a}ndez Gil, Oliver},
  title =	{{The Unification Type of an Equational Theory May Depend on the Instantiation Preorder}},
  booktitle =	{10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025)},
  pages =	{8:1--8:24},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-374-4},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{337},
  editor =	{Fern\'{a}ndez, Maribel},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2025.8},
  URN =		{urn:nbn:de:0030-drops-236230},
  doi =		{10.4230/LIPIcs.FSCD.2025.8},
  annote =	{Keywords: Unification type, Instantiation preorder, Equational theories, Modal and Description Logics}
}
Document
Track A: Algorithms, Complexity and Games
DOI: 10.4230/LIPIcs.ICALP.2025.14
Algorithms for the Diverse-k-SAT Problem: The Geometry of Satisfying Assignments

Authors: Per Austrin, Ioana O. Bercea, Mayank Goswami, Nutan Limaye, and Adarsh Srinivasan

Published in: LIPIcs, Volume 334, 52nd International Colloquium on Automata, Languages, and Programming (ICALP 2025)

Abstract
Given a k-CNF formula and an integer s ≥ 2, we study algorithms that obtain s solutions to the formula that are as dispersed as possible. For s = 2, this problem of computing the diameter of a k-CNF formula was initiated by Creszenzi and Rossi, who showed strong hardness results even for k = 2. The current best upper bound [Angelsmark and Thapper '04] goes to 4ⁿ as k → ∞. As our first result, we show that this quadratic blow up is not necessary by utilizing the Fast-Fourier transform (FFT) to give a O^*(2ⁿ) time exact algorithm for computing the diameter of any k-CNF formula. For s > 2, the problem was raised in the SAT community (Nadel '11) and several heuristics have been proposed for it, but no algorithms with theoretical guarantees are known. We give exact algorithms using FFT and clique-finding that run in O^*(2^{(s-1)n}) and O^*(s² |Ω_{𝐅}|^{ω ⌈ s/3 ⌉}) respectively, where |Ω_{𝐅}| is the size of the solutions space of the formula 𝐅 and ω is the matrix multiplication exponent. However, current SAT algorithms for finding one solution run in time O^*(2^{ε_{k}n}) for ε_{k} ≈ 1-Θ(1/k), which is much faster than all above run times. As our main result, we analyze two popular SAT algorithms - PPZ (Paturi, Pudlák, Zane '97) and Schöning’s ('02) algorithms, and show that in time poly(s)O^*(2^{ε_{k}n}), they can be used to approximate diameter as well as the dispersion (s > 2) problem. While we need to modify Schöning’s original algorithm for technical reasons, we show that the PPZ algorithm, without any modification, samples solutions in a geometric sense. We believe this geometric sampling property of PPZ may be of independent interest. Finally, we focus on diverse solutions to NP-complete optimization problems, and give bi-approximations running in time poly(s)O^*(2^{ε n}) with ε < 1 for several problems such as Maximum Independent Set, Minimum Vertex Cover, Minimum Hitting Set, Feedback Vertex Set, Multicut on Trees and Interval Vertex Deletion. For all of these problems, all existing exact methods for finding optimal diverse solutions have a runtime with at least an exponential dependence on the number of solutions s. Our methods show that by relaxing to bi-approximations, this dependence on s can be made polynomial.
Cite as

Per Austrin, Ioana O. Bercea, Mayank Goswami, Nutan Limaye, and Adarsh Srinivasan. Algorithms for the Diverse-k-SAT Problem: The Geometry of Satisfying Assignments. In 52nd International Colloquium on Automata, Languages, and Programming (ICALP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 334, pp. 14:1-14:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{austrin_et_al:LIPIcs.ICALP.2025.14,
  author =	{Austrin, Per and Bercea, Ioana O. and Goswami, Mayank and Limaye, Nutan and Srinivasan, Adarsh},
  title =	{{Algorithms for the Diverse-k-SAT Problem: The Geometry of Satisfying Assignments}},
  booktitle =	{52nd International Colloquium on Automata, Languages, and Programming (ICALP 2025)},
  pages =	{14:1--14:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-372-0},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{334},
  editor =	{Censor-Hillel, Keren and Grandoni, Fabrizio and Ouaknine, Jo\"{e}l and Puppis, Gabriele},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2025.14},
  URN =		{urn:nbn:de:0030-drops-233916},
  doi =		{10.4230/LIPIcs.ICALP.2025.14},
  annote =	{Keywords: Exponential time algorithms, Satisfiability, k-SAT, PPZ, Sch\"{o}ning, Dispersion, Diversity}
}
Document
Invited Talk
DOI: 10.4230/LIPIcs.ICLP.2010.2
A Logical Paradigm for Systems Biology (Invited Talk)

Authors: François Fages

Published in: LIPIcs, Volume 7, Technical Communications of the 26th International Conference on Logic Programming (2010)

Abstract
Biologists use diagrams to represent complex systems of interaction between molecular species. These graphical notations encompass two types of information: interactions (e.g. protein complexation, modification, binding to a gene, etc.) and regulations (of an interaction or a transcription). Based on these structures, mathematical models can be developed by equipping such molecular interaction networks with kinetic expressions leading to quantitative models of mainly two kinds: ordinary differential equations for a continuous interpretation of the kinetics and continuous-time Markov chains for a stochastic interpretation of the kinetics. Since 2002, we investigate the transposition of programming concepts and tools to the analysis of living processes at the cellular level.
Cite as

François Fages. A Logical Paradigm for Systems Biology (Invited Talk). In Technical Communications of the 26th International Conference on Logic Programming. Leibniz International Proceedings in Informatics (LIPIcs), Volume 7, pp. 2-3, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2010)

Copy BibTex To Clipboard

@InProceedings{fages:LIPIcs.ICLP.2010.2,
  author =	{Fages, Fran\c{c}ois},
  title =	{{A Logical Paradigm for Systems Biology}},
  booktitle =	{Technical Communications of the 26th International Conference on Logic Programming},
  pages =	{2--3},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-17-0},
  ISSN =	{1868-8969},
  year =	{2010},
  volume =	{7},
  editor =	{Hermenegildo, Manuel and Schaub, Torsten},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICLP.2010.2},
  URN =		{urn:nbn:de:0030-drops-25776},
  doi =		{10.4230/LIPIcs.ICLP.2010.2},
  annote =	{Keywords: temporal logic, model-checking, systems biology, hybrid systems}
}
Document
DOI: 10.4230/DagSemProc.06161.3
06161 Working Groups' Report: The Challlenge of Combining Simulation and Verification

Authors: Gregory Batt, Jeremy T. Bradley, Roland Ewald, François Fages, Holger Hermans, Jane Hillston, Peter Kemper, Alke Martens, Pieter Mosterman, Flemming Nielson, Oleg Sokolsky, and Adelinde M. Uhrmacher

Published in: Dagstuhl Seminar Proceedings, Volume 6161, Simulation and Verification of Dynamic Systems (2006)

Abstract
Simulation has found widespread use for experimentation and exploration of the possible impacts of a variety of conditions on a system. In contrast, formal verification is concerned with proving or disproving the correctness of a system with respect to a certain property, using mathematical and logical methods.
Cite as

Gregory Batt, Jeremy T. Bradley, Roland Ewald, François Fages, Holger Hermans, Jane Hillston, Peter Kemper, Alke Martens, Pieter Mosterman, Flemming Nielson, Oleg Sokolsky, and Adelinde M. Uhrmacher. 06161 Working Groups' Report: The Challlenge of Combining Simulation and Verification. In Simulation and Verification of Dynamic Systems. Dagstuhl Seminar Proceedings, Volume 6161, pp. 1-21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2006)

Copy BibTex To Clipboard

@InProceedings{batt_et_al:DagSemProc.06161.3,
  author =	{Batt, Gregory and Bradley, Jeremy T. and Ewald, Roland and Fages, Fran\c{c}ois and Hermans, Holger and Hillston, Jane and Kemper, Peter and Martens, Alke and Mosterman, Pieter and Nielson, Flemming and Sokolsky, Oleg and Uhrmacher, Adelinde M.},
  title =	{{06161 Working Groups' Report: The Challlenge of Combining Simulation and Verification}},
  booktitle =	{Simulation and Verification of Dynamic Systems},
  pages =	{1--21},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2006},
  volume =	{6161},
  editor =	{David M. Nicol and Corrado Priami and Hanne Riis Nielson and Adelinde M. Uhrmacher},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.06161.3},
  URN =		{urn:nbn:de:0030-drops-7249},
  doi =		{10.4230/DagSemProc.06161.3},
  annote =	{Keywords: Modelling, Simulation, Verification, Systemsbiology}
}
Document
DOI: 10.4230/DagSemProc.05371.1
05371 Abstracts Collection – Principles and Practices of Semantic Web Reasoning

Authors: François Bry, François Fages, Massimo Marchiori, and Hans-Jürgen Ohlbach

Published in: Dagstuhl Seminar Proceedings, Volume 5371, Principles and Practices of Semantic Web Reasoning (2006)

Abstract
From 11.09.05 to 16.09.05, the Dagstuhl Seminar 05371 ``Principles and Practices of Semantic Web Reasoning'' % generate automaticall was held in the International Conference and Research Center (IBFI), Schloss Dagstuhl. During the seminar, several participants presented their current research, and ongoing work and open problems were discussed. Abstracts of the presentations given during the seminar as well as abstracts of seminar results and ideas are put together in this paper. The first section describes the seminar topics and goals in general. Links to extended abstracts or full papers are provided, if available.
Cite as

François Bry, François Fages, Massimo Marchiori, and Hans-Jürgen Ohlbach. 05371 Abstracts Collection – Principles and Practices of Semantic Web Reasoning. In Principles and Practices of Semantic Web Reasoning. Dagstuhl Seminar Proceedings, Volume 5371, pp. 1-14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2006)

Copy BibTex To Clipboard

@InProceedings{bry_et_al:DagSemProc.05371.1,
  author =	{Bry, Fran\c{c}ois and Fages, Fran\c{c}ois and Marchiori, Massimo and Ohlbach, Hans-J\"{u}rgen},
  title =	{{05371 Abstracts Collection –  Principles and Practices of Semantic Web Reasoning}},
  booktitle =	{Principles and Practices of Semantic Web Reasoning},
  pages =	{1--14},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2006},
  volume =	{5371},
  editor =	{Fran\c{c}ois Bry and Fran\c{c}ois Fages and Massimo Marchiori and Hans-J\"{u}rgen Ohlbach},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.05371.1},
  URN =		{urn:nbn:de:0030-drops-4813},
  doi =		{10.4230/DagSemProc.05371.1},
  annote =	{Keywords: Semantic Web, reasoning, rules, ontologies, Advanced Web Applications, rule-based reasoning}
}
  • Refine by Type
  • 6 Document/PDF
  • 3 Document/HTML

  • Refine by Publication Year
  • 3 2025
  • 1 2010
  • 2 2006

  • Refine by Author
  • 3 Fages, François
  • 1 Austrin, Per
  • 1 Baader, Franz
  • 1 Batt, Gregory
  • 1 Bercea, Ioana O.
  • Show More...

  • Refine by Series/Journal
  • 4 LIPIcs
  • 2 DagSemProc

  • Refine by Classification
  • 2 Theory of computation → Automated reasoning
  • 1 Applied computing → Systems biology
  • 1 Computing methodologies → Logic programming and answer set programming
  • 1 Theory of computation → Description logics
  • 1 Theory of computation → Design and analysis of algorithms
  • Show More...

  • Refine by Keyword
  • 1 Abstract argumentation
  • 1 Advanced Web Applications
  • 1 Answer set counting
  • 1 Boolean network
  • 1 Computational systems biology
  • 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