4 Search Results for "Martí-Oliet, Narciso"

Document
DOI: 10.4230/LIPIcs.MFCS.2025.55
Model-Theoretic Forcing in Transition Algebra

Authors: Go Hashimoto and Daniel Găină

Published in: LIPIcs, Volume 345, 50th International Symposium on Mathematical Foundations of Computer Science (MFCS 2025)

Abstract
We study Löwenheim-Skolem and Omitting Types theorems in Transition Algebra, a logical system obtained by enhancing many sorted first-order logic with features from dynamic logic. The sentences we consider include compositions, unions, and transitive closures of transition relations, which are treated similarly to actions in dynamic logics to define necessity and possibility operators. We show that Upward Löwenheim-Skolem theorem, any form of compactness, and joint Robinson consistency property fail due to the expressivity of transitive closures of transitions. In this non-compact many-sorted logical system, we develop a forcing technique method by generalizing the classical method of forcing used by Keisler to prove Omitting Types theorem. Instead of working within a single signature, we work with a directed diagram of signatures, which allows us to establish Downward Löwenheim-Skolem and Omitting Types theorems despite the fact that models interpret sorts as sets, possibly empty. Building on a complete system of proof rules for Transition Algebra, we extend it with additional proof rules to reason about constructor-based and/or finite transition algebras. We then establish the completeness of this extended system for a fragment of Transition Algebra obtained by restricting models to constructor-based and/or finite transition algebras.
Cite as

Go Hashimoto and Daniel Găină. Model-Theoretic Forcing in Transition Algebra. In 50th International Symposium on Mathematical Foundations of Computer Science (MFCS 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 345, pp. 55:1-55:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{hashimoto_et_al:LIPIcs.MFCS.2025.55,
  author =	{Hashimoto, Go and G\u{a}in\u{a}, Daniel},
  title =	{{Model-Theoretic Forcing in Transition Algebra}},
  booktitle =	{50th International Symposium on Mathematical Foundations of Computer Science (MFCS 2025)},
  pages =	{55:1--55:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-388-1},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{345},
  editor =	{Gawrychowski, Pawe{\l} and Mazowiecki, Filip and Skrzypczak, Micha{\l}},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2025.55},
  URN =		{urn:nbn:de:0030-drops-241629},
  doi =		{10.4230/LIPIcs.MFCS.2025.55},
  annote =	{Keywords: institutional model theory, algebraic specification, transition algebra, forcing, omitting types property, L\"{o}wenheim-Skolem properties, completeness}
}
Document
System Description
DOI: 10.4230/LIPIcs.FSCD.2019.34
Model Checking Strategy-Controlled Rewriting Systems (System Description)

Authors: Rubén Rubio, Narciso Martí-Oliet, Isabel Pita, and Alberto Verdejo

Published in: LIPIcs, Volume 131, 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)

Abstract
Strategies are widespread in Computer Science. In the domain of reduction and rewriting systems, strategies are studied as recipes to restrict and control reduction steps and rule applications, which are intimately local, in a derivation-global sense. This idea has been exploited by various tools and rewriting-based specification languages, where strategies are an additional specification layer. Systems so described need to be analyzed too. This article discusses model checking of systems controlled by strategies and presents a working strategy-aware LTL model checker for the Maude specification language, based on rewriting logic, and its strategy language.
Cite as

Rubén Rubio, Narciso Martí-Oliet, Isabel Pita, and Alberto Verdejo. Model Checking Strategy-Controlled Rewriting Systems (System Description). In 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 131, pp. 34:1-34:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{rubio_et_al:LIPIcs.FSCD.2019.34,
  author =	{Rubio, Rub\'{e}n and Mart{\'\i}-Oliet, Narciso and Pita, Isabel and Verdejo, Alberto},
  title =	{{Model Checking Strategy-Controlled Rewriting Systems}},
  booktitle =	{4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)},
  pages =	{34:1--34:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-107-8},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{131},
  editor =	{Geuvers, Herman},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2019.34},
  URN =		{urn:nbn:de:0030-drops-105414},
  doi =		{10.4230/LIPIcs.FSCD.2019.34},
  annote =	{Keywords: Model checking, strategies, Maude, rewriting logic}
}
Document
DOI: 10.4230/LITES-v004-i001-a003
Quantitative Analysis of Consistency in NoSQL Key-Value Stores

Authors: Si Liu, Jatin Ganhotra, Muntasir Raihan Rahman, Son Nguyen, Indranil Gupta, and José Meseguer

Published in: LITES, Volume 4, Issue 1 (2017). Leibniz Transactions on Embedded Systems, Volume 4, Issue 1

Abstract
The promise of high scalability and availability has prompted many companies to replace traditional relational database management systems (RDBMS) with NoSQL key-value stores. This comes at the cost of relaxed consistency guarantees: key-value stores only guarantee eventual consistency in principle. In practice, however, many key-value stores seem to offer stronger consistency. Quantifying how well consistency properties are met is a non-trivial problem.  We address this problem by formally modeling key-value stores as probabilistic systems and quantitatively analyzing their consistency properties by both statistical model checking and implementation evaluation. We present for the first time a formal probabilistic model of Apache Cassandra, a popular NoSQL key-value store, and quantify how much Cassandra achieves various consistency guarantees under various conditions. To validate our model, we evaluate multiple consistency properties using two methods and compare them against each other. The two methods are: (1) an implementation-based evaluation of the source code; and (2) a statistical model checking analysis of our probabilistic model.
Cite as

Si Liu, Jatin Ganhotra, Muntasir Raihan Rahman, Son Nguyen, Indranil Gupta, and José Meseguer. Quantitative Analysis of Consistency in NoSQL Key-Value Stores. In LITES, Volume 4, Issue 1 (2017). Leibniz Transactions on Embedded Systems, Volume 4, Issue 1, pp. 03:1-03:26, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@Article{liu_et_al:LITES-v004-i001-a003,
  author =	{Liu, Si and Ganhotra, Jatin and Rahman, Muntasir Raihan and Nguyen, Son and Gupta, Indranil and Meseguer, Jos\'{e}},
  title =	{{Quantitative Analysis of Consistency in NoSQL Key-Value Stores}},
  journal =	{Leibniz Transactions on Embedded Systems},
  pages =	{03:1--03:26},
  ISSN =	{2199-2002},
  year =	{2017},
  volume =	{4},
  number =	{1},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LITES-v004-i001-a003},
  URN =		{urn:nbn:de:0030-drops-192649},
  doi =		{10.4230/LITES-v004-i001-a003},
  annote =	{Keywords: NoSQL Key-value Store, Consistency, Statistical Model Checking, Rewriting Logic, Maude}
}
Document
DOI: 10.4230/LIPIcs.RTA.2010.277
Declarative Debugging of Missing Answers for Maude

Authors: Adrian Riesco, Alberto Verdejo, and Narciso Marti-Oliet

Published in: LIPIcs, Volume 6, Proceedings of the 21st International Conference on Rewriting Techniques and Applications (2010)

Abstract
Declarative debugging is a semi-automatic technique that starts from an incorrect computation and locates a program fragment responsible for the error by building a tree representing this computation and guiding the user through it to find the error. Membership equational logic (MEL) is an equational logic that in addition to equations allows the statement of membership axioms characterizing the elements of a sort. Rewriting logic is a logic of change that extends MEL by adding rewrite rules, that correspond to transitions between states and can be nondeterministic. In this paper we propose a calculus that allows to infer normal forms and least sorts with the equational part, and sets of reachable terms through rules. We use an abbreviation of the proof trees computed with this calculus to build appropriate debugging trees for missing answers (results that are erroneous because they are incomplete), whose adequacy for debugging is proved. Using these trees we have implemented a declarative debugger for Maude, a high-performance system based on rewriting logic, whose use is illustrated with an example.
Cite as

Adrian Riesco, Alberto Verdejo, and Narciso Marti-Oliet. Declarative Debugging of Missing Answers for Maude. In Proceedings of the 21st International Conference on Rewriting Techniques and Applications. Leibniz International Proceedings in Informatics (LIPIcs), Volume 6, pp. 277-294, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2010)

Copy BibTex To Clipboard

@InProceedings{riesco_et_al:LIPIcs.RTA.2010.277,
  author =	{Riesco, Adrian and Verdejo, Alberto and Marti-Oliet, Narciso},
  title =	{{Declarative Debugging of Missing Answers for Maude}},
  booktitle =	{Proceedings of the 21st International Conference on Rewriting Techniques and Applications},
  pages =	{277--294},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-18-7},
  ISSN =	{1868-8969},
  year =	{2010},
  volume =	{6},
  editor =	{Lynch, Christopher},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2010.277},
  URN =		{urn:nbn:de:0030-drops-26589},
  doi =		{10.4230/LIPIcs.RTA.2010.277},
  annote =	{Keywords: Declarative debugging, Maude, Missing answers, Rewriting}
}
  • Refine by Type
  • 4 Document/PDF
  • 1 Document/HTML

  • Refine by Publication Year
  • 1 2025
  • 1 2019
  • 1 2017
  • 1 2010

  • Refine by Author
  • 2 Verdejo, Alberto
  • 1 Ganhotra, Jatin
  • 1 Gupta, Indranil
  • 1 Găină, Daniel
  • 1 Hashimoto, Go
  • Show More...

  • Refine by Series/Journal
  • 3 LIPIcs
  • 1 LITES

  • Refine by Classification
  • 2 Software and its engineering → Model checking
  • 2 Theory of computation → Rewrite systems
  • 1 Computer systems organization → Cloud computing
  • 1 Information systems → Key-value stores
  • 1 Theory of computation → Equational logic and rewriting
  • Show More...

  • Refine by Keyword
  • 3 Maude
  • 1 Consistency
  • 1 Declarative debugging
  • 1 Löwenheim-Skolem properties
  • 1 Missing answers
  • 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