We formalise the notion of enriched coalgebraic modal logic, and determine conditions on the category V (over which we enrich), that allow an enriched logical connection to be extended to a framework for enriched coalgebraic modal logic. Our framework uses V-functors L: A → A and T: X → X, where L determines the modalities of the resulting modal logics, and T determines the coalgebras that provide the semantics. We introduce the V-category Mod(A, α) of models for an L-algebra (A, α), and show that the forgetful V-functor from Mod(A, α) to X creates conical colimits. The concepts of bisimulation, simulation, and behavioural metrics (behavioural approximations),are generalised to a notion of behavioural questions that can be asked of pairs of states in a model. These behavioural questions are shown to arise through choosing the category V to be constructed through enrichment over a commutative unital quantale (Q, Ⓧ, I) in the style of Lawvere (1973). Corresponding generalisations of logical equivalence and expressivity are also introduced,and expressivity of an L-algebra (A, α) is shown to have an abstract category theoretic characterisation in terms of the existence of a so-called behavioural skeleton in the category Mod(A, α). In the resulting framework every model carries the means to compare the behaviour of its states, and we argue that this implies a class of systems is not fully defined until it is specified how states are to be compared or related.
| Identifer | oai:union.ndltd.org:bl.uk/oai:ethos.bl.uk:577269 |
| Date | January 2013 |
| Creators | Wilkinson, Toby |
| Contributors | Cirstea, Corina |
| Publisher | University of Southampton |
| Source Sets | Ethos UK |
| Detected Language | English |
| Type | Electronic Thesis or Dissertation |
| Source | https://eprints.soton.ac.uk/354112/ |
Page generated in 0.0232 seconds