Cognitive Supervisor for an Autonomous Swarm of Robots

As a sequel to our recent work [1], in which a control framework was developed for large-scale joint swarms of unmanned ground (UGV) and aerial (UAV) vehicles, the present paper proposes cognitive and meta-cognitive supervisor models for this kind of distributed robotic system. The cognitive supervisor model is a formalization of the recently Nobel-awarded research in brain science on mammalian and human path integration and navigation, performed by the hippocampus. This is formalized here as an adaptive Hamiltonian path integral, and efficiently simulated for implementation on robotic vehicles as a pair of coupled nonlinear Schr?dinger equations. The meta-cognitive supervisor model is a modal logic of actions and plans that hinges on a weak causality relation that specifies when atoms may change their values without specifying that they must change. This relatively simple logic is decidable yet sufficiently expressive to support the level of inference needed in our application. The atoms and action primitives of the logic framework also provide a straight-forward way of connecting the meta-cognitive supervisor with the cognitive supervisor, with other modules, and to the meta-cognitive supervisors of other robotic platforms in the swarm.

New incremental clustering framework based on induction as inverted deduction

A new incremental clustering framework is presented, the basis of which is the induction as inverted deduction. Induction is inherently risky because it is not truth-preserving. If the clustering is considered as an induction process, the key to build a valid clustering is to minimize the risk of clustering. From the viewpoint of modal logic, the clustering can be described as Kripke frames and Kripke models which are reflexive and symmetric. Based on the theory of modal logic, its properties can be described by system B in syntax. Thus, the risk of clustering can be calculated by the deduction relation of system B and proximity induction theorem described. Since the new proposed framework imposes no additional restrictive conditions of clustering algorithm, it is therefore a universal framework. An incremental clustering algorithm can be easily constructed by this framework from any given nonincremental clustering algorithm. The experiments show that the lower the a priori risk is, the more effective this framework is. It can be demonstrated that this framework is generally valid.

More on Bounding Introspection in Modal Nonmonotonic Logics

By L. we denote the set of all propositional fornmlas. Let C be the set of all clauses. Define C_n=C(Lη:η∈C}.In Sec. 2 of this paper. we prove that for normal modal logics S, the notions of (S. C_)-expansions and S-expansions coincide. In Sec. 3. we prove that if I consists of default clauses then the notions of S-expansions for I and (S.C)-expansions for I coincide. To this end. we first show. in Sec 3.that the notion of S-expansions for I is the same as that of (S.L)-expansions for I.

Using coalgebras and the Giry monad for interpreting game logics a tutorial

The stochastic interpretation of Parikh＇s game logic should not follow the usual pattern of Kripke models, which in turn are based on the Kleisli morphisms for the Giry monad, rather, a specific and more general approach to proba- bilistic nondeterminism is required. We outline this approach together with its probabilistic and measure theoretic basis, in- troducing in a leisurely pace the Giry monad and its Kleisli morphisms together with important techniques for manipu- lating them. Proof establishing specific techniques are given, and pointers to the extant literature are provided. After working through this tutorial, the reader should find it easier to follow the original literature in this and related areas, and it should be possible for her or him to appreciate measure theoretic arguments for original work in the areas of Markov transition systems, and stochastic effectivity func- tions.

Theory of (n) truth degrees of formulas in modal logic and a consistency theorem

The theory of （n） truth degrees of formulas is proposed in modal logic for the first time. A consistency theorem is obtained which says that the （n） truth degree of a modality-free formula equals the truth degree of the formula in two-valued propositional logic. Variations of （n） truth degrees of formulas w.r.t. n in temporal logic is investigated. Moreover, the theory of （n） similarity degrees among modal formulas is proposed and the （n） modal logic metric space is derived therefrom which contains the classical logic metric space as a subspace. Finally, a kind of approximate reasoning theory is proposed in modal logic.

The Global Properties of Valid Formulas in Modal Logic K

Global property is the necessary condition which must be satisfied by the provable formulas. It can help to find out some unprovable formula that does not satisfy some global property before proving it using formal automated rea-soning systems, thus the efficiency of the whole system is improved. This paper presents some global properties of valid formulas in modal logic K. Such prop-erties are structure characters of formulas, so they are simple and easy to check.At the same time, some global properties of K unsatisfiable formula set are also given.

Lattice-Valued Modal Propositional Logic Based on M-Lattice Implication Algebras

The modal lattice implication algebra(i.e.,M-lattice implication algebra) is introduced and its properties are investigated.The modal lattice-valued propositional logical system is introduced by considering the M-lattice implication algebra as the valuation field,and the syntax and semantic of the logical system are discussed,respectively.

On decidability and model checking for a first order modal logic for value-passing processes

A semantic interpretation of a first order extension of Hennessy-Milner logic for value-passing processes, named HML(FO), is presented. The semantics is based on symbolic transition graphs with assignment. It is shown that the satisfiability of the two-variable sub-logic HML(FO2) of HML(FO) is decidable, and the complexity discussed. Finally, a decision procedure for model checking the value-passing processes with respect to HML(FO2) is obtained.

A Logical Characterization for Linear Higher-Order Processes

Modal logic characterization in a higher-order setting is usually not a trivial task because higher-order process-passing is quite different from first-order name-passing. We study the logical characterization of higherorder processes constrained by linearity. Linearity respects resource-sensitiveness and does not allow processes to duplicate themselves arbitrarily. We provide a modal logic that characterizes linear higher-order processes,particularly the bisimulation called local bisimulation over them. More importantly, the logic has modalities for higher-order actions downscaled to resembling first-order ones in Hennessy-Milner logic, based on a formulation exploiting the linearity of processes.

A predicate spatial logic for mobile processes

A modal logic for describing temporal as well as spatial properties of mobileprocesses, expressed in the asynchronous π-calculus, is presented. The logic has recur-sive constructs built upon predicate-variables. The semantics of the logic is establishedand shown to be monotonic, thus guarantees the existence of fixpoints. An algorithm isdeveloped to automatically check if a mobile process has properties described as formulasin the logic. The correctness of the algorithm is proved.