1,721,041 research outputs found
A Presheaf Semantics for Quantified Temporal Logics
No full textTemporal logics encompass a family of formalisms for the verification of computational devices, and its quantified extensions allow to reason about the properties of individual components of a system. The expressiveness of these logics poses problems in identifying a semantics that exploits its features without imposing restrictions on the acceptable behaviours. We address this issue by introducing a counterpart-based semantics and we provide a categorical presentation of such semantics in terms of relational presheaves
Pisa, 1954-1961: Assessing key stages of a seminal Italian project
No full textThe last decade and half has seen a renewed interest in the development of the IT industry in Italy and in the role of the 1950s pioneers. The aim of the article is to retrace key stages of the first Italian project aimed at creating an electronic calculator, carried out by the University of Pisa in collaboration with Olivetti. The re-evaluation of the documents kept in the University's archives, including the technical projects, has proved fruitful and has shed light on lesser-known aspects of a project that opened the way to the birth of Computer Science in the country as a business and as a scientific discipline
Specification and modelling of computing systems through graphs and graph transformation
No full textThis special issue collects extended versions of selected papers presented at the 14th International Conference on Graph Transformation (ICGT 2021), held on June 24 and 25, 2021, as a virtual event due to ongoing COVID-19 countermeasures and travel restrictions
Special issue on Application-oriented aspects of graphs and graph transformation (ICGT 2020)
No full textConcurrent semantics for fusions: Weak prime domains and connected event structures
No full textStable event structures, and their duality with prime algebraic domains, represent a landmark of concurrency theory, since they provide a neat characterisation of causality in computations. As such, they have been used for defining the concurrent semantics of many formalisms, from Petri nets to (linear) graph rewriting systems. Stability however is restrictive for formalisms with “fusion”, where a computational step may merge parts of the state. This happens e.g. for graph rewriting systems with non-linear rules, which are used to cover some relevant applications (such as the graphical encoding of calculi with name passing). Guided by the need of giving semantics to such formalisms, we leave aside stability and characterise a class of domains, referred to as weak prime domains, naturally generalising prime algebraic domains. We then identify a corresponding class of event structures, that we call connected event structures, via a duality result formalised as an equivalence of categories
Petri nets are dioids
No full textIn a seminal paper Montanari and Meseguer showed that an algebraic interpretation of Petri nets in terms of commutative monoids can be used to provide an elegant characterisation of the deterministic computations of a net, accounting for their sequential and parallel composition. Here we show that, along the same lines, by adding an (idempotent) operation and thus taking dioids (commutative semirings) rather than monoids, one can faithfully characterise the non-deterministic computations of a Petri net
Graph Rewriting Components
No full textWe introduce a component model for graph rewriting that allows to model a system as a network of components with interfaces representing shared views of internal states and transformations. Their composition assembles a global view whose behaviour is equivalent to the synchronised distributed execution of local components in the network. Formally, components are arrows in a category with interfaces as objects that, with suitable component connectors, forms a Frobenius algebra. This allows the use of string diagrams to model the architecture of basic components and connectors, such that their assembly is freely generated by the algebraic structure. The compositionality of the proposed model is reflected by Structural Operational Semantic rules
- …
