Search Results

Documents authored by Orejas, Fernando

Document
DOI: 10.4230/LIPIcs.CONCUR.2024.39
Coinductive Techniques for Checking Satisfiability of Generalized Nested Conditions

Authors: Lara Stoltenow, Barbara König, Sven Schneider, Andrea Corradini, Leen Lambers, and Fernando Orejas

Published in: LIPIcs, Volume 311, 35th International Conference on Concurrency Theory (CONCUR 2024)

Abstract
We study nested conditions, a generalization of first-order logic to a categorical setting, and provide a tableau-based (semi-decision) procedure for checking (un)satisfiability and finite model generation. This generalizes earlier results on graph conditions. Furthermore we introduce a notion of witnesses, allowing the detection of infinite models in some cases. To ensure completeness, paths in a tableau must be fair, where fairness requires that all parts of a condition are processed eventually. Since the correctness arguments are non-trivial, we rely on coinductive proof methods and up-to techniques that structure the arguments. We distinguish between two types of categories: categories where all sections are isomorphisms, allowing for a simpler tableau calculus that includes finite model generation; in categories where this requirement does not hold, model generation does not work, but we still obtain a sound and complete calculus.
Cite as

Lara Stoltenow, Barbara König, Sven Schneider, Andrea Corradini, Leen Lambers, and Fernando Orejas. Coinductive Techniques for Checking Satisfiability of Generalized Nested Conditions. In 35th International Conference on Concurrency Theory (CONCUR 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 311, pp. 39:1-39:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{stoltenow_et_al:LIPIcs.CONCUR.2024.39,
  author =	{Stoltenow, Lara and K\"{o}nig, Barbara and Schneider, Sven and Corradini, Andrea and Lambers, Leen and Orejas, Fernando},
  title =	{{Coinductive Techniques for Checking Satisfiability of Generalized Nested Conditions}},
  booktitle =	{35th International Conference on Concurrency Theory (CONCUR 2024)},
  pages =	{39:1--39:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-339-3},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{311},
  editor =	{Majumdar, Rupak 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.CONCUR.2024.39},
  URN =		{urn:nbn:de:0030-drops-208113},
  doi =		{10.4230/LIPIcs.CONCUR.2024.39},
  annote =	{Keywords: satisfiability, graph conditions, coinductive techniques, category theory}
}
Document
DOI: 10.4230/DagSemRep.288
Semi-Formal and Formal Specification Techniques for Software Systems (Dagstuhl Seminar 00411)

Authors: Hartmut Ehrig, Gregor Engels, Fernando Orejas, and Martin Wirsing

Published in: Dagstuhl Seminar Reports. Dagstuhl Seminar Reports, Volume 1 (2021)

Abstract
Cite as

Hartmut Ehrig, Gregor Engels, Fernando Orejas, and Martin Wirsing. Semi-Formal and Formal Specification Techniques for Software Systems (Dagstuhl Seminar 00411). Dagstuhl Seminar Report 288, pp. 1-36, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2001)

Copy BibTex To Clipboard

@TechReport{ehrig_et_al:DagSemRep.288,
  author =	{Ehrig, Hartmut and Engels, Gregor and Orejas, Fernando and Wirsing, Martin},
  title =	{{Semi-Formal and Formal Specification Techniques for Software Systems (Dagstuhl Seminar 00411)}},
  pages =	{1--36},
  ISSN =	{1619-0203},
  year =	{2001},
  type = 	{Dagstuhl Seminar Report},
  number =	{288},
  institution =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemRep.288},
  URN =		{urn:nbn:de:0030-drops-151724},
  doi =		{10.4230/DagSemRep.288},
}
Document
DOI: 10.4230/DagSemRep.218
Semi-Formal and Formal Specification Techniques for Software Systems (Dagstuhl Seminar 98281)

Authors: Hartmut Ehrig, Gergor Engels, Fernando Orejas, and Martin Wirsing

Published in: Dagstuhl Seminar Reports. Dagstuhl Seminar Reports, Volume 1 (2021)

Abstract
Cite as

Hartmut Ehrig, Gergor Engels, Fernando Orejas, and Martin Wirsing. Semi-Formal and Formal Specification Techniques for Software Systems (Dagstuhl Seminar 98281). Dagstuhl Seminar Report 218, pp. 1-40, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (1998)

Copy BibTex To Clipboard

@TechReport{ehrig_et_al:DagSemRep.218,
  author =	{Ehrig, Hartmut and Engels, Gergor and Orejas, Fernando and Wirsing, Martin},
  title =	{{Semi-Formal and Formal Specification Techniques for Software Systems (Dagstuhl Seminar 98281)}},
  pages =	{1--40},
  ISSN =	{1619-0203},
  year =	{1998},
  type = 	{Dagstuhl Seminar Report},
  number =	{218},
  institution =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemRep.218},
  URN =		{urn:nbn:de:0030-drops-151043},
  doi =		{10.4230/DagSemRep.218},
}
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

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