Search

We introduce a new concept in the area of formal logic: axioms for model morphisms. We work in the setting of specification languages that define the semantics of a theory as a category of models. While it is routine to use axioms to specify the class of models of a theory, there has so far been no analogue to systematically specify the morphisms between these models. This leads to subtle problems where it is difficult to give a theory that specifies the intended model category, or where seemingly isomorphic theories actually have non-isomorphic model categories. Our morphism axioms remedy this by providing new syntax for axiomatizing and reasoning about the properties of model morphisms. Additionally, our system resolves a subtle incompatibility between theory morphisms and model morphisms: the semantics that maps theories to model categories is functorial. While this result is standard in principle, previous formulations had to restrict the allowed theory morphisms or the allowed model morphisms. Our system allows establishing the result in full generality. [ABSTRACT FROM AUTHOR]

Although there have been many works on bounded semantics, a characterization of a good definition for a bounded semantics has not been given, and this has led to definitions of bounded semantics of temporal logics that may not be appropriate with respect to the potential usefulness as a basis for developing bounded model checking approaches. On the other side, the research effort on bounded semantics has mainly focused on existentially interpreted fragments of temporal logics, due to the intricacy of defining appropriate bounded semantics for universally interpreted fragments, or for temporal logics with path quantifiers that are closed under negation. This work addresses these two problems, by defining the characteristics of bounded semantics for clarifying the concept of bounded semantics, and presenting a bounded semantics for the full set of CTL, a logic closed under negation, including possibility for specifying both existential and universal properties. [ABSTRACT FROM AUTHOR]

Abstract: The calculus of Mobile Ambients has been introduced for expressing mobility and mobile computation. In this paper we present a probabilistic version of Mobile Ambients by augmenting the syntax of the original Ambient Calculus with a (guarded) probabilistic choice operator. To allow for the representation of both the probabilistic behaviour introduced through the new probabilistic choice operator and the nondeterminism present in the original Ambient Calculus we use probabilistic automata as the underpinning semantic model. The Ambient logic is a logic for Mobile Ambients that contains a novel treatment of both locations and hidden names. For specifying properties of Probabilistic Mobile Ambients, we extend this logic to specify probabilistic behaviour. In addition, to show the utility of our approach we present an example of a virus infecting a network. [Copyright &y& Elsevier]

Abstract: Monadic least fixed point logic MLFP is a natural logic whose expressiveness lies between that of first-order logic FO and monadic second-order logic MSO. In this paper, we take a closer look at the expressive power of MLFP. Our results are: [(1)] MLFP can describe graph properties beyond any fixed level of the monadic second-order quantifier alternation hierarchy. [(2)] On strings with built-in addition, MLFP can describe at least all languages that belong to the linear time complexity class DLIN. [(3)] Settling the question whether or, equivalently, settling the question whether would solve open problems in complexity theory: “” would imply that whereas “” would imply that . Apart from this we give a self-contained proof of the previously known result that MLFP is strictly less expressive than MSO on the class of finite graphs. [Copyright &y& Elsevier]