Subscribe to the gold package and get unlimited access to Shamra Academy
Register a new userMetrics for Formal Structures, with an Application to Kripke Models and their Dynamics
108
0
0.0
(
0
)
Added by
Rasmus Kr{\\ae}mmer Rendsvig
Publication date
2017
fields
and research's language is
English
Ask ChatGPT about the research
No Arabic abstract
This report introduces and investigates a family of metrics on sets of pointed Kripke models. The metrics are generalizations of the Hamming distance applicable to countably infinite binary strings and, by extension, logical theories or semantic structures. We first study the topological properties of the resulting metric spaces. A key result provides sufficient conditions for spaces having the Stone property, i.e., being compact, totally disconnected and Hausdorff. Second, we turn to mappings, where it is shown that a widely used type of model transformations, product updates, give rise to continuous maps in the induced topology.
rate research
Read More
We consider the operation of sum on Kripke frames, where a family of frames-summands is indexed by elements of another frame. In many cases, the modal logic of sums inherits the finite model property and decidability from the modal logic of summands. In this paper we show that, under a general condition, the satisfiability problem on sums is polynomial space Turing reducible to the satisfiability problem on summands. In particular, for many modal logics decidability in PSPACE is an immediate corollary from the semantic characterization of the logic.
Modularity is a central principle throughout the design process for cyber-physical systems. Modularity reduces complexity and increases reuse of behavior. In this paper we pose and answer the following question: how can we identify independent `modules within the structure of reactive control architectures? To this end, we propose a graph-structured control architecture we call a decision structure, and show how it generalises some reactive control architectures which are popular in Artificial Intelligence (AI) and robotics, specifically Teleo-Reactive programs (TRs), Decision Trees (DTs), Behavior Trees (BTs) and Generalised Behavior Trees ($k$-BTs). Inspired by the definition of a module in graph theory, we define modules in decision structures and show how each decision structure possesses a canonical decomposition into its modules. We can naturally characterise each of the BTs, $k$-BTs, DTs and TRs by properties of their module decomposition. This allows us to recognise which decision structures are equivalent to each of these architectures in quadratic time. Our proposed concept of modules extends to formal verification, under any verification scheme capable of verifying a decision structure. Namely, we prove that a modification to a module within a decision structure has no greater flow-on effects than a modification to an individual action within that structure. This enables verification on modules to be done locally and hierarchically, where structures can be verified and then repeatedly locally modified, with modules replaced by modules while preserving correctness. To illustrate the findings, we present an example of a solar-powered drone controlled by a decision structure. We use a Linear Temporal Logic-based verification scheme to verify the correctness of this structure, and then show how one can modify modules while preserving its correctness.
This paper concerns branching simulation for weighted Kripke structures with parametric weights. Concretely, we consider a weighted extension of branching simulation where a single transitions can be matched by a sequence of transitions while preserving the branching behavior. We relax this notion to allow for a small degree of deviation in the matching of weights, inducing a directed distance on states. The distance between two states can be used directly to relate properties of the states within a sub-fragment of weighted CTL. The problem of relating systems thus changes to minimizing the distance which, in the general parametric case, corresponds to finding suitable parameter valuations such that one system can approximately simulate another. Although the distance considers a potentially infinite set of transition sequences we demonstrate that there exists an upper bound on the length of relevant sequences, thereby establishing the computability of the distance.
There are several cutting edge applications needing PCA methods for data on tori and we propose a novel torus-PCA method with important properties that can be generally applied. There are two existing general methods: tangent space PCA and geodesic PCA. However, unlike tangent space PCA, our torus-PCA honors the cyclic topology of the data space whereas, unlike geodesic PCA, our torus-PCA produces a variety of non-winding, non-dense descriptors. This is achieved by deforming tori into spheres and then using a variant of the recently developed principle nested spheres analysis. This PCA analysis involves a step of small sphere fitting and we provide an improved test to avoid overfitting. However, deforming tori into spheres creates singularities. We introduce a data-adaptive pre-clustering technique to keep the singularities away from the data. For the frequently encountered case that the residual variance around the PCA main component is small, we use a post-mode hunting technique for more fine-grained clustering. Thus in general, there are three successive interrelated key steps of torus-PCA in practice: pre-clustering, deformation, and post-mode hunting. We illustrate our method with two recently studied RNA structure (tori) data sets: one is a small RNA data set which is established as the benchmark for PCA and we validate our method through this data. Another is a large RNA data set (containing the small RNA data set) for which we show that our method provides interpretable principal components as well as giving further insight into its structure.
In the literature, there have been several methods and definitions for working out if two theories are equivalent (essentially the same) or not. In this article, we do something subtler. We provide means to measure distances (and explore connections) between formal theories. We introduce two main notions for such distances. The first one is that of textit{axiomatic distance}, but we argue that it might be of limited interest. The more interesting and widely applicable notion is that of textit{conceptual distance} which measures the minimum number of concepts that distinguish two theories. For instance, we use conceptual distance to show that relativistic and classical kinematics are distinguished by one concept only. We also develop further notions of distance, and we include a number of suggestions for applying and extending our project.
Log in to be able to interact and post comments
comments
Fetching comments
Sign in to be able to follow your search criteria
