110 research outputs found
Report on Coalgebraic Methods in Computer Science 2022
Full text linkThe 16th edition of the IFIP WG 1.3 International Workshop on Coalgebraic Methods in Computer Science (CMCS 2022) took place in Munich on Saturday April 2 and Sunday April 3, 2022, as a satellite event of the European Joint Conference on Theory and Practice of Software (ETAPS 2022). As chairs of the workshop, it was a great pleasure for us to run the workshop as an on-site event after a long hiatus due to the COVID pandemic. The workshop was, in fact, a hybrid event, allowing both speakers and registered participants to participate remotely, but in-person participation was strongly encouraged, partly through ETAPS registration fees being the same for online and on-site participation. Up until just a few weeks before the workshop, the COVID situation in Munich was still quite uncertain, and we did not know how many people would attend on-site or at all, so we were extremely happy to find that the large majority of speakers and participants chose to travel to the event, which ensured a lively and engaging atmosphere. The workshop had circa 40 participants of which 5 participated online (with an attendance of 20--30 throughout the sessions). This made CMCS the second-largest workshop at ETAPS 2022. The hybrid setup did pose some technical challenges, but it was much appreciated, and without the option of presenting on-line at least three of the talks would have had to be cancelled. A hybrid format will be considered also for future editions of the workshop
Bisimulation for Weakly Expressive Coalgebraic Modal Logics
Full text linkResearch on the expressiveness of coalgebraic modal logics with respect to semantic equivalence notions has so far focused mainly on finding logics that are able to distinguish states that are not behaviourally equivalent (such logics are said to be expressive). In other words, the notion of behavioural equivalence is taken as the starting point, and the expressiveness of the logic is evaluated against it.
However, for some applications, modal logics that are not expressive are of independent interest. Such an example is given by contingency logic.
We can now turn the question of expressiveness around and ask, given a modal logic, what is a suitable notion of semantic equivalence? In this paper, we propose a notion of \Lambda-bisimulation which is parametric in a collection
\Lambda of predicate liftings. We study the basic properties of \Lambda-bisimilarity, and prove as our main result a Hennessy-Milner style theorem, which shows that (for finitary functors) \Lambda-bisimilarity exactly matches the expressiveness of the coalgebraic modal logic arising from \Lambda
Algebraic Presentation of Semifree Monads
Full text linkMonads and their composition via distributive laws have many applications in
program semantics and functional programming. For many interesting monads,
distributive laws fail to exist, and this has motivated investigations into
weaker notions. In this line of research, Petri\c{s}an and Sarkis recently
introduced a construction called the semifree monad in order to study
semialgebras for a monad and weak distributive laws. In this paper, we prove
that an algebraic presentation of the semifree monad M^s on a monad M can be
obtained uniformly from an algebraic presentation of M. This result was
conjectured by Petri\c{s}an and Sarkis. We also show that semifree monads are
ideal monads, that the semifree construction is not a monad transformer, and
that the semifree construction is a comonad on the category of monads.Comment: In Proceedings of CMCS 202
Unambiguous acceptance of thin coalgebras
No full textAutomata admitting at most one accepting run per structure, known as unambiguous automata, find applications in ver- ification of reactive systems as they extend the class of deterministic automata whilst maintaining some of their desirable properties. In this paper, we generalise a classical construction of unambiguous automata from thin trees to thin coalgebras for analytic functors. This achieves two goals: extending the existing construction to a larger class of structures, and pro- viding conceptual clarity and parametricity to the construction by formalising it in the coalgebraic framework. As part of the construction, we link automaton acceptance of languages of thin coalgebras to language recognition via so-called coherent algebras, which were previously introduced for studying thin coalgebras. This link also allows us to establish an automata- theoretic characterisation of languages recognised by finite coherent algebras
Conditional Obligations in Justification Logic
No full textThis paper presents a justification counterpart for dyadic deontic logic, which is often argued to be better than Standard Deontic Logic at representing conditional and contrary-to-duty obligations, such as those exemplified by the notorious Chisholm's puzzle. We consider the alethic-deontic system (E) and present the explicit version of this system (JE) by replacing the alethic Box-modality with proof terms and the dyadic deontic Circ-modality with justification terms. The explicit representation of strong factual detachment (SFD) is given and finally soundness and completeness of the system (JE) with respect to basic models and preference models is established
Towards verb modification in frames: A case study on German “schlagen” (to hit)
Full text linkHit-verbs have three basic meaning components, namely movement, contact and force (e.g. [12], Levin 1993), which interact with the verbs’ argument structure in various ways. In this paper, we map out the different grammatical constructions of the German verb schlagen (usually, though loosely, translated as ‘hit’; also ‘beat’, ‘strike’) and their restrictions on agentivity and the force component. Using modification by pure manner adverbs as a tool to test for possible default values of the force component, and agent-oriented adverbs to discover possible interactions with agentivity, we show that German schlagen is rather liberal with respect to its force component. Crucially, the force component may not only be modified by standard, force-denoting manner adverbs such as lightly and hard, but also through agent-oriented adverbs such as playfully, via a defeasible inference. We show further that our findings can be profitably modelled in Frame Semantics, a framework which is especially well suited for modelling a fine-grained decomposition of word meaning, including the manner-related components of verbs
- …
