179 research outputs found

    Co-Algebraic Models for Quantitative Spatial Logics,

    No full text
    AbstractWe introduce a class of coalgebraic models and a family of modal logics that support the specification of spatial properties of distributed applications. The evaluation of a formula yields a value in a suitable multi-valued algebraic structure, giving a measure of the satisfaction of a requirement, induced by the decomposition of a system into subsystems, meant as available resources. As semantic domain we consider certain algebraic structures, called c-semirings, that allow us to generalize boolean logics to the multi-valued case, while keeping a number of the axioms of boolean algebras. Under suitable conditions on the structure of c-semirings, we show that, even if our logical formalisms are equipped with spatial operators, the interpretation of formulas fully characterizes bisimilarity

    Storytelling & Worldmaking: The World-building Activity as a Design Practice

    No full text
    Living in a highly mediated world, we are witnessing the rise of new consumption behaviour and the spread of multichannel narrative forms. A scenario in which audiences enter vicariously imaginary worlds, exploring the fictional spaces conveyed through multiple channels. Starting with the recognition of the difference between story and storyworld, this article aims to describe the worldbuilding activity, the process of creating imaginary worlds, as a design practice

    Symmetries, local names and dynamic (de)-allocation of names

    No full text
    The semantics of name-passing calculi is often defined employing coalgebraic models over presheaf categories This elegant theory lacks finiteness properties hence it is not apt to implementation Coalgebras over named sets, called history-dependent automata are better suited for the purpose due to locality of names A theory of behavioural functors for named sets is still lacking the semantics of each language has been given in an ad-hoc way and algorithms were implemented only for the pi-calculus Existence of the final coalgebra for the pi-calculus was never proved We introduce a language of accessible functors to specify history-dependent automata in a modular way leading to a clean formulation and a generalisation of previous results and to the proof of existence of a final coalgebra in a wide range of cases (C) 2010 Elsevier Inc All rights reserve

    Improving the RST-OIL algorithm for oil spill detection under severe sun glint conditions

    No full text
    In recent years, the risk related to oil spill accidents has significantly increased due to a global growth in offshore extraction and oil maritime transport. To ensure sea safety, the implementation of a monitoring system able to provide real-time coverage of large areas and a timely alarm in case of accidents is of major importance. Satellite remote sensing, thanks to its inherent peculiarities, has become an essential component in such a system. Recently, the general Robust Satellite Technique (RST) approach has been successfully applied to oil spill detection (RST-OIL) using optical band satellite data. In this paper, an advanced configuration of RST-OIL is presented, and we aim to extend its applicability to a larger set of observation conditions, referring, in particular, to those in the presence of severe sun glint effects that generate some detection limits to the RST-OIL standard algorithm. To test such a configuration, the DeepWater Horizon platform accident from April 2010 was selected as a test case. We analyzed a time series of Moderate Resolution Imaging Spectroradiometer (MODIS) images that are usually significantly affected by sun glint in the Gulf of Mexico area. The accuracy of the achieved results was evaluated for comparison with a well-established satellite methodology based on microwave data, which confirms the potential of the proposed approach in identifying the oil presence on the scene with good accuracy and reliability, even in these severe conditions

    Lymph node fine needle cytology, Epstein Barr virus infection and Hodgkin Lymphoma

    No full text
    Epstein-Barr virus (EBV) is a double-strand DNA virus of the herpes family; it is one of the most common human viruses and it is associated with a wide spectrum of benign and malignant conditions. EBV is related to the development of several neoplasms, globally 1% of tumours, including lymphoproliferative, epithelial and mesenchymal neoplasm. Lymphoproliferative disorders include Hodgkin lymphoma (HL) and B and T cell non-Hodgkin lymphoma. HL is one of the most common lymphoma in the developed world, affecting both young people and adults. HL pathogenesis is complex and includes various and partially unknown mechanisms. EBV has been detected in some HL neoplastic cells and expresses genes with a potential oncogenic function, therefore many studies suggest that viral infections have a causative role in neoplastic transformation. Fine Needle Cytology (FNC) is extensively used in the first diagnosis of any lymph-nodal enlargement, including reactive lymphadeno - pathies and lymphoproliferative processes; therefore cytopathologists are likely to encounter EBVassociated malignancies in cytology samples, mainly HL, which is one of the most common lymphoma. This study focuses on the cytological features and ancillary studies required to diagnose EBV-related HL

    Towards a Spatial Model Checker on GPU

    No full text
    The tool VoxLogicA merges the state-of-the-art library of computational imaging algorithms ITK with the combination of declarative specification and optimised execution provided by spatial logic model checking. The analysis of an existing benchmark for segmentation of brain tumours via a simple logical specification reached very high accuracy. We introduce a new, GPU-based version of VoxLogicA and present preliminary results on its implementation, scalability, and applications

    Event-Based Choreography

    No full text
    An important feature of the service-oriented approach is the ability to aggregate, through programmable coordination patterns, the activities involved in service interactions. Two different approaches can be adopted to tackle service coordination: orchestration and choreography. In this paper, we introduce a formal methodology to handle coordination among services from the perspective of a global observer, in the spirit of choreography models. In particular, we address the problem of verifying compliance and consistency between the design of service interactions and the choreography constraints
    corecore