Showing 1–17 of 17 results for author: Sano, K

VERTECS: A COTS-based payload interface board to enable next generation astronomical imaging payloads

Authors: Ezra Fielding, Victor H. Schulz, Keenan A. A. Chatar, Kei Sano, Akitoshi Hanazawa

Abstract: Due to advances in observation and imaging technologies, modern astronomical satellites generate large volumes of data. This necessitates efficient onboard data processing and high-speed data downlink. Reflecting this trend is the VERTECS 6U Astronomical Nanosatellite. Designed for the observation of Extragalactic Background Light (EBL), this mission is expected to generate a substantial amount of… ▽ More Due to advances in observation and imaging technologies, modern astronomical satellites generate large volumes of data. This necessitates efficient onboard data processing and high-speed data downlink. Reflecting this trend is the VERTECS 6U Astronomical Nanosatellite. Designed for the observation of Extragalactic Background Light (EBL), this mission is expected to generate a substantial amount of image data, particularly within the confines of CubeSat capabilities. This paper introduces the VERTECS Camera Control Board (CCB), an open-source payload interface board leveraging Commercial Off-The-Shelf (COTS) components, with a Raspberry Pi Compute Module 4 at its core. The VERTECS CCB hardware and software have been designed from the ground up to serve as the sole interface between the VERTECS bus system and astronomical imaging payload, while providing compute capability not usually seen in nanosatellites of this class. Responsible for mission data processing, it will facilitate high-speed data transfer from the imaging payload via gigabit Ethernet, while also providing a high-bitrate serial connection to the payload X-band transmitter for mission data downlink. Additional interfaces for secondary payloads are provided via USB-C and standard 15-pin camera connectors. The Raspberry Pi embedded within the VERTECS CCB operates on a standard Linux distribution, streamlining the software development process. Beyond addressing the current mission's payload control and data handling requirements, the CCB sets the stage for future missions with heightened data demands. Furthermore, it supports the adoption of machine learning and other compute-intensive applications in orbit. This paper delves into the development of the VERTECS CCB, offering insights into the design and validation of this next-generation payload interface, to ensure that it can survive the rigors of space flight. △ Less

Submitted 2 June, 2024; originally announced June 2024.

Comments: 10 pages, to be presented at SPIE Software and Cyberinfrastructure for Astronomy VIII

Spatio-temporal reconstruction of substance dynamics using compressed sensing in multi-spectral magnetic resonance spectroscopic imaging

Authors: Utako Yamamoto, Hirohiko Imai, Kei Sano, Masayuki Ohzeki, Tetsuya Matsuda, Toshiyuki Tanaka

Abstract: The objective of our study is to observe dynamics of multiple substances in vivo with high temporal resolution from multi-spectral magnetic resonance spectroscopic imaging (MRSI) data. The multi-spectral MRSI can effectively separate spectral peaks of multiple substances and is useful to measure spatial distributions of substances. However it is difficult to measure time-varying substance distribu… ▽ More The objective of our study is to observe dynamics of multiple substances in vivo with high temporal resolution from multi-spectral magnetic resonance spectroscopic imaging (MRSI) data. The multi-spectral MRSI can effectively separate spectral peaks of multiple substances and is useful to measure spatial distributions of substances. However it is difficult to measure time-varying substance distributions directly by ordinary full sampling because the measurement requires a significantly long time. In this study, we propose a novel method to reconstruct the spatio-temporal distributions of substances from randomly undersampled multi-spectral MRSI data on the basis of compressed sensing (CS) and the partially separable function model with base spectra of substances. In our method, we have employed spatio-temporal sparsity and temporal smoothness of the substance distributions as prior knowledge to perform CS. The effectiveness of our method has been evaluated using phantom data sets of glass tubes filled with glucose or lactate solution in increasing amounts over time and animal data sets of a tumor-bearing mouse to observe the metabolic dynamics involved in the Warburg effect in vivo. The reconstructed results are consistent with the expected behaviors, showing that our method can reconstruct the spatio-temporal distribution of substances with a temporal resolution of four seconds which is extremely short time scale compared with that of full sampling. Since this method utilizes only prior knowledge naturally assumed for the spatio-temporal distributions of substances and is independent of the number of the spectral and spatial dimensions or the acquisition sequence of MRSI, it is expected to contribute to revealing the underlying substance dynamics in MRSI data already acquired or to be acquired in the future. △ Less

Submitted 1 March, 2024; originally announced March 2024.

Journal ref: Expert Systems with Applications, Vol. 232 (2023) p. 120744

How many views does your deep neural network use for prediction?

Authors: Keisuke Kawano, Takuro Kutsuna, Keisuke Sano

Abstract: The generalization ability of Deep Neural Networks (DNNs) is still not fully understood, despite numerous theoretical and empirical analyses. Recently, Allen-Zhu & Li (2023) introduced the concept of multi-views to explain the generalization ability of DNNs, but their main target is ensemble or distilled models, and no method for estimating multi-views used in a prediction of a specific input is d… ▽ More The generalization ability of Deep Neural Networks (DNNs) is still not fully understood, despite numerous theoretical and empirical analyses. Recently, Allen-Zhu & Li (2023) introduced the concept of multi-views to explain the generalization ability of DNNs, but their main target is ensemble or distilled models, and no method for estimating multi-views used in a prediction of a specific input is discussed. In this paper, we propose Minimal Sufficient Views (MSVs), which is similar to multi-views but can be efficiently computed for real images. MSVs is a set of minimal and distinct features in an input, each of which preserves a model's prediction for the input. We empirically show that there is a clear relationship between the number of MSVs and prediction accuracy across models, including convolutional and transformer models, suggesting that a multi-view like perspective is also important for understanding the generalization ability of (non-ensemble or non-distilled) DNNs. △ Less

Submitted 1 February, 2024; originally announced February 2024.

Comments: 20 pages

Semantic Incompleteness of Hilbert System for a Combination of Classical and Intuitionistic Propositional Logic

Authors: Masanobu Toyooka, Katsuhiko Sano

Abstract: The updated version of this paper has already been published in The Australasian Journal of Logic. You can access to the paper from the following link: https://ojs.victoria.ac.nz/ajl/article/view/7696. This paper shows Hilbert system $(\mathbf{C+J})^{-}$, given by del Cerro and Herzig (1996) is semantically incomplete. This system is proposed as a proof theory for Kripke semantics for a combinat… ▽ More The updated version of this paper has already been published in The Australasian Journal of Logic. You can access to the paper from the following link: https://ojs.victoria.ac.nz/ajl/article/view/7696. This paper shows Hilbert system $(\mathbf{C+J})^{-}$, given by del Cerro and Herzig (1996) is semantically incomplete. This system is proposed as a proof theory for Kripke semantics for a combination of intuitionistic and classical propositional logic, which is obtained by adding the natural semantic clause of classical implication into intuitionistic Kripke semantics. Although Hilbert system $(\mathbf{C+J})^{-}$ contains intuitionistic modus ponens as a rule, it does not contain classical modus ponens. This paper gives an argument ensuring that the system $(\mathbf{C+J})^{-}$ is semantically incomplete because of the absence of classical modus ponens. Our method is based on the logic of paradox, which is a paraconsistent logic proposed by Priest (1979). △ Less

Submitted 26 December, 2023; v1 submitted 15 July, 2022; originally announced July 2022.

Comments: 9 pages

Combining First-Order Classical and Intuitionistic Logic

Authors: Masanobu Toyooka, Katsuhiko Sano

Abstract: This paper studies a first-order expansion of a combination C+J of intuitionistic and classical propositional logic, which was studied by Humberstone (1979) and del Cerro and Herzig (1996), from a proof-theoretic viewpoint. While C+J has both classical and intuitionistic implications, our first-order expansion adds classical and intuitionistic universal quantifiers and one existential quantifier t… ▽ More This paper studies a first-order expansion of a combination C+J of intuitionistic and classical propositional logic, which was studied by Humberstone (1979) and del Cerro and Herzig (1996), from a proof-theoretic viewpoint. While C+J has both classical and intuitionistic implications, our first-order expansion adds classical and intuitionistic universal quantifiers and one existential quantifier to C+J. This paper provides a multi-succedent sequent calculus G(FOC+J) for our combination of the first-order intuitionistic and classical logic. Our sequent calculus G(FOC+J) restricts contexts of the right rules for intuitionistic implication and intuitionistic universal quantifier to particular forms of formulas. The cut-elimination theorem is established to ensure the subformula property. As a corollary, G(FOC+J) is conservative over both first-order intuitionistic and classical logic. Strong completeness of G(FOC+J) is proved via a canonical model argument. △ Less

Submitted 13 April, 2022; originally announced April 2022.

Comments: In Proceedings NCL 2022, arXiv:2204.06359

Journal ref: EPTCS 358, 2022, pp. 25-40

A Balance for Fairness: Fair Distribution Utilising Physics in Games of Characteristic Function Form

Authors: Song-Ju Kim, Taiki Takahashi, Kazuo Sano

Abstract: In chaotic modern society, there is an increasing demand for the realization of true 'fairness'. In Greek mythology, Themis, the 'goddess of justice', has a sword in her right hand to protect society from vices, and a 'balance of judgment' in her left hand that measures good and evil. In this study, we propose a fair distribution method 'utilising physics' for the profit in games of characteristic… ▽ More In chaotic modern society, there is an increasing demand for the realization of true 'fairness'. In Greek mythology, Themis, the 'goddess of justice', has a sword in her right hand to protect society from vices, and a 'balance of judgment' in her left hand that measures good and evil. In this study, we propose a fair distribution method 'utilising physics' for the profit in games of characteristic function form. Specifically, we show that the linear programming problem for calculating 'nucleolus' can be efficiently solved by considering it as a physical system in which gravity works. In addition to being able to significantly reduce computational complexity thereby, we believe that this system could have flexibility necessary to respond to real-time changes in the parameter. △ Less

Submitted 5 February, 2021; v1 submitted 27 January, 2021; originally announced January 2021.

Comments: 13 pages, 5 figures

White Paper from Workshop on Large-scale Parallel Numerical Computing Technology (LSPANC 2020): HPC and Computer Arithmetic toward Minimal-Precision Computing

Authors: Roman Iakymchuk, Daichi Mukunoki, Artur Podobas, Fabienne Jézéquel, Toshiyuki Imamura, Norihisa Fujita, Jens Huthmann, Shuhei Kudo, Yiyu Tan, Jens Domke, Kai Torben Ohlhus, Takeshi Fukaya, Takeo Hoshi, Yuki Murakami, Maho Nakata, Takeshi Ogita, Kentaro Sano, Taisuke Boku

Abstract: In numerical computations, precision of floating-point computations is a key factor to determine the performance (speed and energy-efficiency) as well as the reliability (accuracy and reproducibility). However, precision generally plays a contrary role for both. Therefore, the ultimate concept for maximizing both at the same time is the minimal-precision computing through precision-tuning, which a… ▽ More In numerical computations, precision of floating-point computations is a key factor to determine the performance (speed and energy-efficiency) as well as the reliability (accuracy and reproducibility). However, precision generally plays a contrary role for both. Therefore, the ultimate concept for maximizing both at the same time is the minimal-precision computing through precision-tuning, which adjusts the optimal precision for each operation and data. Several studies have been already conducted for it so far (e.g. Precimoniuos and Verrou), but the scope of those studies is limited to the precision-tuning alone. Hence, we aim to propose a broader concept of the minimal-precision computing system with precision-tuning, involving both hardware and software stack. In 2019, we have started the Minimal-Precision Computing project to propose a more broad concept of the minimal-precision computing system with precision-tuning, involving both hardware and software stack. Specifically, our system combines (1) a precision-tuning method based on Discrete Stochastic Arithmetic (DSA), (2) arbitrary-precision arithmetic libraries, (3) fast and accurate numerical libraries, and (4) Field-Programmable Gate Array (FPGA) with High-Level Synthesis (HLS). In this white paper, we aim to provide an overview of various technologies related to minimal- and mixed-precision, to outline the future direction of the project, as well as to discuss current challenges together with our project members and guest speakers at the LSPANC 2020 workshop; https://www.r-ccs.riken.jp/labs/lpnctrt/lspanc2020jan/. △ Less

Submitted 11 April, 2020; v1 submitted 9 April, 2020; originally announced April 2020.

Report number: hal-02536316

A Survey on Coarse-Grained Reconfigurable Architectures from a Performance Perspective

Authors: Artur Podobas, Kentaro Sano, Satoshi Matsuoka

Abstract: With the end of both Dennard's scaling and Moore's law, computer users and researchers are aggressively exploring alternative forms of computing in order to continue the performance scaling that we have come to enjoy. Among the more salient and practical of the post-Moore alternatives are reconfigurable systems, with Coarse-Grained Reconfigurable Architectures (CGRAs) seemingly capable of striking… ▽ More With the end of both Dennard's scaling and Moore's law, computer users and researchers are aggressively exploring alternative forms of computing in order to continue the performance scaling that we have come to enjoy. Among the more salient and practical of the post-Moore alternatives are reconfigurable systems, with Coarse-Grained Reconfigurable Architectures (CGRAs) seemingly capable of striking a balance between performance and programmability. In this paper, we survey the landscape of CGRAs. We summarize nearly three decades of literature on the subject, with a particular focus on the premise behind the different CGRAs and how they have evolved. Next, we compile metrics of available CGRAs and analyze their performance properties in order to understand and discover knowledge gaps and opportunities for future CGRA research specialized towards High-Performance Computing (HPC). We find that there are ample opportunities for future research on CGRAs, in particular with respect to size, functionality, support for parallel programming models, and to evaluate more complex applications. △ Less

Submitted 15 September, 2020; v1 submitted 9 April, 2020; originally announced April 2020.

ACM Class: A.1; B.0; C.1; C.3

Journal ref: IEEE Access, 2020 (https://ieeexplore.ieee.org/document/9149601)

A Guide of Fingerprint Based Radio Emitter Localization using Multiple Sensors

Authors: Tao Yu, Azril Haniz, Kentaro Sano, Ryosuke Iwata, Ryouta Kosaka, Yusuke Kuki, Gia Khanh Tran, Jun-Ichi Takada, Kei Sakaguchi

Abstract: Location information is essential to varieties of applications. It is one of the most important context to be detected by wireless distributed sensors, which is a key technology in Internet-of-Things. Fingerprint-based methods, which compare location unique fingerprints collected beforehand with the fingerprint measured from the target, have attracted much attention recently in both of academia an… ▽ More Location information is essential to varieties of applications. It is one of the most important context to be detected by wireless distributed sensors, which is a key technology in Internet-of-Things. Fingerprint-based methods, which compare location unique fingerprints collected beforehand with the fingerprint measured from the target, have attracted much attention recently in both of academia and industry. They have been successfully used for many location-based applications.From the viewpoint of practical applications, in this paper, four different typical approaches of fingerprint-based radio emitter localization system are introduced with four different representative applications: localization of LTE smart phone used for anti-cheating in exams, indoor localization of Wi-Fi terminals, localized light control in BEMS using location information of occupants, and illegal radio localization in outdoor environments. Based on the different practical application scenarios, different solutions, which are designed to enhance the localization performance, are discussed in detail. To the best of the authors' knowledge, this is the first paper to give a guideline for readers about fingerprint-based localization system in terms of fingerprint selection, hardware architecture design and algorithm enhancement △ Less

Submitted 5 April, 2018; originally announced April 2018.

Comments: This paper is accepted by IEICE Transactions on Communications

Journal ref: IEICE Trans. Commun., IEICE, Vol. E101-B, No.10, Oct. 2018

Axiomatizing Epistemic Logic of Friendship via Tree Sequent Calculus

Authors: Katsuhiko Sano

Abstract: This paper positively solves an open problem if it is possible to provide a Hilbert system to Epistemic Logic of Friendship (EFL) by Seligman, Girard and Liu. To find a Hilbert system, we first introduce a sound, complete and cut-free tree (or nested) sequent calculus for EFL, which is an integrated combination of Seligman's sequent calculus for basic hybrid logic and a tree sequent calculus for m… ▽ More This paper positively solves an open problem if it is possible to provide a Hilbert system to Epistemic Logic of Friendship (EFL) by Seligman, Girard and Liu. To find a Hilbert system, we first introduce a sound, complete and cut-free tree (or nested) sequent calculus for EFL, which is an integrated combination of Seligman's sequent calculus for basic hybrid logic and a tree sequent calculus for modal logic. Then we translate a tree sequent into an ordinary formula to specify a Hilbert system of EFL and finally show that our Hilbert system is sound and complete for the intended two-dimensional semantics. △ Less

Submitted 10 July, 2019; v1 submitted 24 April, 2017; originally announced April 2017.

Comments: 24 pages, 1 figure

Strong Completeness and the Finite Model Property for Bi-Intuitionistic Stable Tense Logics

Authors: Katsuhiko Sano, John G. Stell

Abstract: Bi-Intuitionistic Stable Tense Logics (BIST Logics) are tense logics with a Kripke semantics where worlds in a frame are equipped with a pre-order as well as with an accessibility relation which is 'stable' with respect to this pre-order. BIST logics are extensions of a logic, BiSKt, which arose in the semantic context of hypergraphs, since a special case of the pre-order can represent the inci… ▽ More Bi-Intuitionistic Stable Tense Logics (BIST Logics) are tense logics with a Kripke semantics where worlds in a frame are equipped with a pre-order as well as with an accessibility relation which is 'stable' with respect to this pre-order. BIST logics are extensions of a logic, BiSKt, which arose in the semantic context of hypergraphs, since a special case of the pre-order can represent the incidence structure of a hypergraph. In this paper we provide, for the first time, a Hilbert-style axiomatisation of BISKt and prove the strong completeness of BiSKt. We go on to prove strong completeness of a class of BIST logics obtained by extending BiSKt by formulas of a certain form. Moreover we show that the finite model property and the decidability hold for a class of BIST logics. △ Less

Submitted 6 March, 2017; originally announced March 2017.

Comments: In Proceedings M4M9 2017, arXiv:1703.01736

Journal ref: EPTCS 243, 2017, pp. 105-121

Model Theory and Proof Theory of Coalgebraic Predicate Logic

Authors: Tadeusz Litak, Dirk Pattinson, Katsuhiko Sano, Lutz Schröder

Abstract: We propose a generalization of first-order logic originating in a neglected work by C.C. Chang: a natural and generic correspondence language for any types of structures which can be recast as Set-coalgebras. We discuss axiomatization and completeness results for several natural classes of such logics. Moreover, we show that an entirely general completeness result is not possible. We study the exp… ▽ More We propose a generalization of first-order logic originating in a neglected work by C.C. Chang: a natural and generic correspondence language for any types of structures which can be recast as Set-coalgebras. We discuss axiomatization and completeness results for several natural classes of such logics. Moreover, we show that an entirely general completeness result is not possible. We study the expressive power of our language, both in comparison with coalgebraic hybrid logics and with existing first-order proposals for special classes of Set-coalgebras (apart from relational structures, also neighbourhood frames and topological spaces). Basic model-theoretic constructions and results, in particular ultraproducts, obtain for the two classes that allow completeness---and in some cases beyond that. Finally, we discuss a basic sequent system, for which we establish a syntactic cut-elimination result. △ Less

Submitted 19 March, 2018; v1 submitted 13 January, 2017; originally announced January 2017.

Journal ref: Logical Methods in Computer Science, Volume 14, Issue 1 (March 20, 2018) lmcs:2645

DSL-based Design Space Exploration for Temporal and Spatial Parallelism of Custom Stream Computing

Authors: Kentaro Sano

Abstract: Stream computation is one of the approaches suitable for FPGA-based custom computing due to its high throughput capability brought by pipelining with regular memory access. To increase performance of iterative stream computation, we can exploit both temporal and spatial parallelism by deepening and duplicating pipelines, respectively. However, the performance is constrained by several factors incl… ▽ More Stream computation is one of the approaches suitable for FPGA-based custom computing due to its high throughput capability brought by pipelining with regular memory access. To increase performance of iterative stream computation, we can exploit both temporal and spatial parallelism by deepening and duplicating pipelines, respectively. However, the performance is constrained by several factors including available hardware resources on FPGA, an external memory bandwidth, and utilization of pipeline stages, and therefore we need to find the best mix of the different parallelism to achieve the highest performance per power. In this paper, we present a domain-specific language (DSL) based design space exploration for temporally and/or spatially parallel stream computation with FPGA. We define a DSL where we can easily design a hierarchical structure of parallel stream computation with abstract description of computation. For iterative stream computation of fluid dynamics simulation, we design hardware structures with a different mix of the temporal and spatial parallelism. By measuring the performance and the power consumption, we find the best among them. △ Less

Submitted 27 August, 2015; originally announced September 2015.

Comments: Presented at Second International Workshop on FPGAs for Software Programmers (FSP 2015) (arXiv:1508.06320)

Report number: FSP/2015/06

Characterising Modal Definability of Team-Based Logics via the Universal Modality

Authors: Katsuhiko Sano, Jonni Virtema

Abstract: We study model and frame definability of various modal logics. Let ML(A+) denote the fragment of modal logic extended with the universal modality in which the universal modality occurs only positively. We show that a class of Kripke models is definable in ML(A+) if and only if the class is elementary and closed under disjoint unions and surjective bisimulations. We also characterise the definabili… ▽ More We study model and frame definability of various modal logics. Let ML(A+) denote the fragment of modal logic extended with the universal modality in which the universal modality occurs only positively. We show that a class of Kripke models is definable in ML(A+) if and only if the class is elementary and closed under disjoint unions and surjective bisimulations. We also characterise the definability of ML(A+) in the spirit of the well-known Goldblatt--Thomason theorem. We show that an elementary class F of Kripke frames is definable in ML(A+) if and only if F is closed under taking generated subframes and bounded morphic images, and reflects ultrafilter extensions and finitely generated subframes. In addition we study frame definability relative to finite transitive frames and give an analogous characterisation of ML(A+)-definability relative to finite transitive frames. Finally, we initiate the study of model and frame definability in team-based logics. We study (extended) modal dependence logic, (extended) modal inclusion logic, and modal team logic. We establish strict linear hierarchies with respect to model definability and frame definability, respectively. We show that, with respect to model and frame definability, the before mentioned team-based logics, except modal dependence logic, either coincide with ML(A+) or plain modal logic ML. Thus as a corollary we obtain model theoretic characterisation of model and frame definability for the team-based logics. △ Less

Submitted 21 February, 2018; v1 submitted 27 February, 2015; originally announced February 2015.

Comments: 30 pages. This is a preprint of a journal article to appear in Annals of Pure and Applied Logic. The preprint combines and extends two conference papers arXiv:1502.07884v1 and arXiv:1606.05140. The title of this preprint is changed to reflect this

Axiomatizing Propositional Dependence Logics

Authors: Katsuhiko Sano, Jonni Virtema

Abstract: We give sound and complete Hilbert-style axiomatizations for propositional dependence logic (PD), modal dependence logic (MDL), and extended modal dependence logic (EMDL) by extending existing axiomatizations for propositional logic and modal logic. In addition, we give novel labeled tableau calculi for PD, MDL, and EMDL. We prove soundness, completeness and termination for each of the labeled cal… ▽ More We give sound and complete Hilbert-style axiomatizations for propositional dependence logic (PD), modal dependence logic (MDL), and extended modal dependence logic (EMDL) by extending existing axiomatizations for propositional logic and modal logic. In addition, we give novel labeled tableau calculi for PD, MDL, and EMDL. We prove soundness, completeness and termination for each of the labeled calculi. △ Less

Submitted 19 October, 2014; originally announced October 2014.

Comments: 15 pages

Stream Processor Generator for HPC to Embedded Applications on FPGA-based System Platform

Authors: Kentaro Sano, Hayato Suzuki, Ryo Ito, Tomohiro Ueno, Satoru Yamamoto

Abstract: This paper presents a stream processor generator, called SPGen, for FPGA-based system-on-chip platforms. In our research project, we use an FPGA as a common platform for applications ranging from HPC to embedded/robotics computing. Pipelining in application-specific stream processors brings FPGAs power-efficient and high-performance computing. However, poor productivity in develo** custom pipeli… ▽ More This paper presents a stream processor generator, called SPGen, for FPGA-based system-on-chip platforms. In our research project, we use an FPGA as a common platform for applications ranging from HPC to embedded/robotics computing. Pipelining in application-specific stream processors brings FPGAs power-efficient and high-performance computing. However, poor productivity in develo** custom pipelines prevents the reconfigurable platform from being widely and easily used. SPGen aims at assisting developers to design and implement high-throughput stream processors by generating their HDL codes with our domain-specific high-level stream processing description, called SPD.With an example of fluid dynamics computation, we validate SPD for describing a real application and verify SPGen for synthesis with a pipelined data-flow graph. We also demonstrate that SPGen allows us to easily explore a design space for finding better implementation than a hand-designed one. △ Less

Submitted 21 August, 2014; originally announced August 2014.

Comments: Presented at First International Workshop on FPGAs for Software Programmers (FSP 2014) (arXiv:1408.4423)

Report number: FSP/2014/09

The Expressive Power of Modal Dependence Logic

Authors: Lauri Hella, Kerkko Luosto, Katsuhiko Sano, Jonni Virtema

Abstract: We study the expressive power of various modal logics with team semantics. We show that exactly the properties of teams that are downward closed and closed under team k-bisimulation, for some finite k, are definable in modal logic extended with intuitionistic disjunction. Furthermore, we show that the expressive power of modal logic with intuitionistic disjunction and extended modal dependence log… ▽ More We study the expressive power of various modal logics with team semantics. We show that exactly the properties of teams that are downward closed and closed under team k-bisimulation, for some finite k, are definable in modal logic extended with intuitionistic disjunction. Furthermore, we show that the expressive power of modal logic with intuitionistic disjunction and extended modal dependence logic coincide. Finally we establish that any translation from extended modal dependence logic into modal logic with intuitionistic disjunction increases the size of some formulas exponentially. △ Less

Submitted 24 June, 2014; originally announced June 2014.

Comments: 19 pages