2 Search Results for "Codescu, Mihai"

Document

Track B: Automata, Logic, Semantics, and Theory of Programming

DOI: 10.4230/LIPIcs.ICALP.2024.143

Forcing, Transition Algebras, and Calculi

Authors: Go Hashimoto, Daniel Găină, and Ionuţ Ţuţu

Published in: LIPIcs, Volume 297, 51st International Colloquium on Automata, Languages, and Programming (ICALP 2024)

Abstract

We bring forward a logical system of transition algebras that enhances many-sorted first-order logic using features from dynamic logics. The sentences we consider include compositions, unions, and transitive closures of transition relations, which are treated similarly to the actions used in dynamic logics in order to define necessity and possibility operators. This leads to a higher degree of expressivity than that of many-sorted first-order logic. For example, one can finitely axiomatize both the finiteness and the reachability of models, neither of which are ordinarily possible in many-sorted first-order logic. We introduce syntactic entailment and study basic properties such as compactness and completeness, showing that the latter does not hold when standard finitary proof rules are used. Consequently, we define proof rules having both finite and countably infinite premises, and we provide conditions under which completeness can be proved. To that end, we generalize the forcing method introduced in model theory by Robinson from a single signature to a category of signatures, and we apply it to obtain a completeness result for signatures that are at most countable.

Cite as

Go Hashimoto, Daniel Găină, and Ionuţ Ţuţu. Forcing, Transition Algebras, and Calculi. In 51st International Colloquium on Automata, Languages, and Programming (ICALP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 297, pp. 143:1-143:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{hashimoto_et_al:LIPIcs.ICALP.2024.143,
  author =	{Hashimoto, Go and G\u{a}in\u{a}, Daniel and \c{T}u\c{t}u, Ionu\c{t}},
  title =	{{Forcing, Transition Algebras, and Calculi}},
  booktitle =	{51st International Colloquium on Automata, Languages, and Programming (ICALP 2024)},
  pages =	{143:1--143:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-322-5},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{297},
  editor =	{Bringmann, Karl and Grohe, Martin and Puppis, Gabriele and Svensson, Ola},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2024.143},
  URN =		{urn:nbn:de:0030-drops-202868},
  doi =		{10.4230/LIPIcs.ICALP.2024.143},
  annote =	{Keywords: Forcing, institution theory, calculi, algebraic specification, transition systems}
}

Document

Tool Paper

DOI: 10.4230/LIPIcs.CALCO.2019.17

Hybridisation of Institutions in HETS (Tool Paper)

Authors: Mihai Codescu

Published in: LIPIcs, Volume 139, 8th Conference on Algebra and Coalgebra in Computer Science (CALCO 2019)

Abstract

We present a tool for the specification and verification of reconfigurable systems. The foundation of the tool is provided by a generic method, called hybridisation of institutions, of extending an arbitrary base institution with features characteristic to hybrid logic, both at the syntactic and the semantic level. Automated proof support for hybridised institutions is obtained via a generic lifting of encodings to first-order logic from the base institution to the hybridised institution. We describe how hybridisation and lifting of encodings to first-order logic are implemented in an extension of the Heterogeneous Tool Set in their full generality. We illustrate the formalism thus obtained with the specification and verification of an autonomous car driving system for highways.

Cite as

Mihai Codescu. Hybridisation of Institutions in HETS (Tool Paper). In 8th Conference on Algebra and Coalgebra in Computer Science (CALCO 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 139, pp. 17:1-17:10, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{codescu:LIPIcs.CALCO.2019.17,
  author =	{Codescu, Mihai},
  title =	{{Hybridisation of Institutions in HETS}},
  booktitle =	{8th Conference on Algebra and Coalgebra in Computer Science (CALCO 2019)},
  pages =	{17:1--17:10},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-120-7},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{139},
  editor =	{Roggenbach, Markus and Sokolova, Ana},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2019.17},
  URN =		{urn:nbn:de:0030-drops-114451},
  doi =		{10.4230/LIPIcs.CALCO.2019.17},
  annote =	{Keywords: hybrid logics, formal verification, institutions, reconfigurable systems}
}

Refine by Author
1 Codescu, Mihai
1 Găină, Daniel
1 Hashimoto, Go
1 Ţuţu, Ionuţ

Refine by Classification
2 Theory of computation → Logic and verification
1 Software and its engineering → Specification languages
1 Theory of computation → Algebraic semantics
1 Theory of computation → Equational logic and rewriting
1 Theory of computation → Proof theory

Refine by Keyword
1 Forcing
1 algebraic specification
1 calculi
1 formal verification
1 hybrid logics
Show More...

Refine by Type
2 document

Refine by Publication Year
1 2019
1 2024