Subscribe to the gold package and get unlimited access to Shamra Academy
Register a new userA Spatial Logic for a Simplicial Complex Model
413
0
0.0
(
0
)
Added by
Michele Loreti
Publication date
2021
fields
Informatics Engineering
and research's language is
English
Ask ChatGPT about the research
No Arabic abstract
Collective adaptive systems (CAS) consist of many heterogeneous components typically organised in groups. These entities interact with each other by adapting their behaviour to pursue individual or collective goals. The distribution of system entities determines a space that can be either physical or logical. The former is defined in terms of a physical relation among components. The latter depends on some logical relations such as being part of the same group. For these systems, specification and verification of spatial properties play a fundamental role to understand their behaviour and to support their design. Recently, different tools and languages have been introduced to specify and verify the properties of space. However, these formalisms are mainly based on graphs. This does not permit considering higher-order relations such as surfaces or volumes. In this work, we propose a spatial logic interpreted on simplicial complexes. These are topological objects able to represent surfaces and volumes efficiently and that generalise graphs with higher-order edges. The expressiveness of the proposed spatial logic is studied in terms of bisimulation and branching bisimulation relations defined over simplicial complexes. Finally, we discuss how the satisfaction of logical formulas can be verified by a correct and complete algorithm.
rate research
Read More
The standard semantics of multi-agent epistemic logic $S5$ is based on Kripke models whose accessibility relations are reflexive, symmetric and transitive. This one dimensional structure contains implicit higher-dimensional information beyond pairwise interactions, that has been formalized as pure simplicial models in previous work from the authors. Here we extend the theory to encompass all simplicial models - including the ones that are not pure. The corresponding Kripke models are those where the accessibility relation is symmetric and transitive, but might not be reflexive. This yields the epistemic logic $KB4$ which can reason about situations where some of the agents may die.
We propose a new graph-based spatial temporal logic for knowledge representation and automated reasoning in this paper. The proposed logic achieves a balance between expressiveness and tractability in applications such as cognitive robots. The satisfiability of the proposed logic is decidable. We apply a Hilbert style axiomatization for the proposed graph-based spatial temporal logic, in which Modus ponens and IRR are the inference rules. We show that the corresponding deduction system is sound and complete and can be implemented through SAT.
This paper is concerned with the first-order paraconsistent logic LPQ$^{supset,mathsf{F}}$. A sequent-style natural deduction proof system for this logic is presented and, for this proof system, both a model-theoretic justification and a logical justification by means of an embedding into first-order classical logic is given. For no logic that is essentially the same as LPQ$^{supset,mathsf{F}}$, a natural deduction proof system is currently available in the literature. The given embedding provides both a classical-logic explanation of this logic and a logical justification of its proof system. The major properties of LPQ$^{supset,mathsf{F}}$ are also treated.
We propose a model of the substructural logic of Bunched Implications (BI) that is suitable for reasoning about quantum states. In our model, the separating conjunction of BI describes separable quantum states. We develop a program logic where pre- and post-conditions are BI formulas describing quantum states -- the program logic can be seen as a counterpart of separation logic for imperative quantum programs. We exercise the logic for proving the security of quantum one-time pad and secret sharing, and we show how the program logic can be used to discover a flaw in Google Cirqs tutorial on the Variational Quantum Algorithm (VQA).
Most modern (classical) programming languages support recursion. Recursion has also been successfully applied to the design of several quantum algorithms and introduced in a couple of quantum programming languages. So, it can be expected that recursion will become one of the fundamental paradigms of quantum programming. Several program logics have been developed for verification of non-recursive quantum programs. However, there are as yet no general methods for reasoning about recursive procedures in quantum computing. We fill the gap in this paper by presenting a logic for recursive quantum programs. This logic is an extension of quantum Hoare logic for quantum While-programs. The (relative) completeness of the logic is proved, and its effectiveness is shown by a running example: fixed-point Grovers search.
Log in to be able to interact and post comments
comments
Fetching comments
Sign in to be able to follow your search criteria
