A doctrinal approach to modal/temporal Heyting logic and non-determinism in processes. (27th February 2017)

• Record Type: Journal Article
• Authors: BOTTONI, PAOLO; GORLA, DANIELE; KASANGIAN, STEFANO; LABELLA, ANNA
• Is Part Of: Mathematical structures in computer science. Volume 28:Number 4(2018)
• Page Start: 508
• Page End: 532
• Publication Date: 2017-02-27
• Subjects: Computer science -- Mathematics -- Periodicals; 004.015105
• DOI: 10.1017/S0960129517000019
• Languages: English
• ISSNs: 0960-1295

Abstract

Abstract : The study of algebraic modelling of labelled non-deterministic concurrent processes leads us to consider a category LB, obtained from a complete meet-semilatticeB and fromB -valued equivalence relations. We prove that, ifB 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.