The study of algebraic modelling of labelled non-deterministic concurrent processes leads us to consider a category LB , obtained from a complete meet-semilattice B and from B-valued equivalence relations. We prove that, if B has enough properties, then LB presents a two-fold internal logical structure, induced by two doctrines definable on it: one related to its families of subobjects and one to its families of regular subobjects. The first doctrine is Heyting and makes LB a Heyting category, the second one is Boolean. We will see that the difference between these two logical structures, namely the different behaviour of the negation operator, can be interpreted in terms of a distinction between non-deterministic and deterministic behaviours of agents able to perform computations in the context of the same process. Moreover, the sorted first-order logic naturally associated with LB can be extended to a modal/temporal logic, again using the doctrinal setting. Relations are also drawn to other computational models
A doctrinal approach to modal/temporal Heyting logic and non-determinism in processes / Bottoni, Paolo Gaspare; Gorla, Daniele; Kasangian, Stefano; Labella, Anna. - In: MATHEMATICAL STRUCTURES IN COMPUTER SCIENCE. - ISSN 0960-1295. - ELETTRONICO. - 28:4(2018), pp. 508-532. [10.1017/S0960129517000019]
A doctrinal approach to modal/temporal Heyting logic and non-determinism in processes
BOTTONI, Paolo Gaspare;GORLA, DANIELE;LABELLA, Anna
2018
Abstract
The study of algebraic modelling of labelled non-deterministic concurrent processes leads us to consider a category LB , obtained from a complete meet-semilattice B and from B-valued equivalence relations. We prove that, if B has enough properties, then LB presents a two-fold internal logical structure, induced by two doctrines definable on it: one related to its families of subobjects and one to its families of regular subobjects. The first doctrine is Heyting and makes LB a Heyting category, the second one is Boolean. We will see that the difference between these two logical structures, namely the different behaviour of the negation operator, can be interpreted in terms of a distinction between non-deterministic and deterministic behaviours of agents able to perform computations in the context of the same process. Moreover, the sorted first-order logic naturally associated with LB can be extended to a modal/temporal logic, again using the doctrinal setting. Relations are also drawn to other computational modelsFile | Dimensione | Formato | |
---|---|---|---|
Bottoni_doctrinal_2018.pdf
accesso aperto
Tipologia:
Documento in Post-print (versione successiva alla peer review e accettata per la pubblicazione)
Licenza:
Tutti i diritti riservati (All rights reserved)
Dimensione
257.84 kB
Formato
Adobe PDF
|
257.84 kB | Adobe PDF |
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.