Geometric Model Checking of Continuous Space

Autor: Nick Bezhanishvili, Vincenzo Ciancia, David Gabelaia, Gianluca Grilletti, Diego Latella, Mieke Massink

Publikováno v: Logical Methods in Computer Science, Vol Volume 18, Issue 4 (2022)

Topological Spatial Model Checking is a recent paradigm where model checking techniques are developed for the topological interpretation of Modal Logic. The Spatial Logic of Closure Spaces, SLCS, extends Modal Logic with reachability connectives that

Externí odkaz: https://doaj.org/article/57108e6df75746e8824662401f131dc3

Completeness for the Classical Antecedent Fragment of Inquisitive First-Order Logic

Autor: Gianluca Grilletti

Publikováno v: Journal of Logic, Language and Information

Inquisitive first order logic "Equation missing" is an extension of first order classical logic, introducing questions and studying the logical relations between questions and quantifiers. It is not known whether "Equation missing" is recursively axi

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::9daae5e7d19c012f37b410f395b2d927
https://doi.org/10.1007/s10849-021-09341-y

Games and cardinalities in inquisitive first-order logic

Autor: Ivano Ciardelli, Gianluca Grilletti

Publikováno v: The Review of Symbolic Logic
Review of Symbolic Logic, 16(1), 241-267. Cambridge University Press

Inquisitive first-order logic, InqBQ, is a system which extends classical first-order logic with formulas expressing questions. From a mathematical point of view, formulas in this logic express properties of sets of relational structures. This paper

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::16c2b0b0fbe45d77c481f043a2acda6f
https://hdl.handle.net/11577/3453988

Spatio-temporal model checking of vehicular movement in public transport systems

Autor: Vincenzo Ciancia, Diego Latella, Mieke Massink, Michele Loreti, Stephen Gilmore, Gianluca Grilletti

Publikováno v: International journal on software tools for technology transfer (Internet) 20 (2018): 289–311. doi:10.1007/s10009-018-0483-8
info:cnr-pdr/source/autori:Ciancia V. ; Gilmore S.; Grilletti G.; Latella D.; Loreti M.; Massink M./titolo:Spatio-temporal model checking of vehicular movement in public transport systems/doi:10.1007%2Fs10009-018-0483-8/rivista:International journal on software tools for technology transfer (Internet)/anno:2018/pagina_da:289/pagina_a:311/intervallo_pagine:289–311/volume:20
International Journal on Software Tool for Technology Transfer, 20(3). Springer
Ciancia, V, Gilmore, S, Griletti, G, Latella, D, Loreti, M & Massink, M 2018, ' Spatio-temporal model-checking of vehicular movement in public transport systems ', International Journal on Software Tools for Technology Transfer, vol. 20, no. 3, pp. 289-311 . https://doi.org/10.1007/s10009-018-0483-8

We present the use of a novel spatio-temporal model-checker to detect problems in the data and operation of a collective adaptive system. Data correctness is important to ensure operational correctness in systems which adapt in response to data. We i

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::be141d51b27decb26c44ea5f944e467d
https://doi.org/10.1007/s10009-018-0483-8

An experimental spatio-temporal model checker

Autor: Michele Loreti, Gianluca Grilletti, Mieke Massink, Diego Latella, Vincenzo Ciancia

Publikováno v: Software Engineering and Formal Methods, edited by Domenico Bianculli, Radu Calinescu, Bernhard Rumpe, pp. 297–311, 2015
info:cnr-pdr/source/autori:Ciancia V.; Grilletti G.; Latella D.; Loreti M.; Massink M./titolo:An experimental spatio-temporal model checker/titolo_volume:Software Engineering and Formal Methods/curatori_volume:Domenico Bianculli, Radu Calinescu, Bernhard Rumpe/editore:/anno:2015
Software Engineering and Formal Methods ISBN: 9783662492239
SEFM Workshops

In this work we present a spatial extension of the global model checking algorithm of the temporal logic CTL. This classical veri- fication framework is augmented with ideas coming from the tradition of topological spatial logics. More precisely, we

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::417210f2cc213a14238329eba84744a8
https://openportal.isti.cnr.it/doc?id=people______::8507bc21d252e7900aa186246630c103