Kyushu University Academic Staff Educational and Research Activities Database
Researcher information (To researchers) Need Help? How to update
Daniel Mircea GAINA Last modified date:2020.07.08





E-Mail *Since the e-mail address is not displayed in Internet Explorer, please use another web browser:Google Chrome, safari.
Homepage
https://kyushu-u.pure.elsevier.com/en/persons/daniel-mircea-gaina
 Reseacher Profiling Tool Kyushu University Pure
http://imi.kyushu-u.ac.jp/~daniel/
Phone
092-802-4425
Fax
092-802-4405
Academic Degree
PhD in information science from Japan Advanced Institute of Science and Technology
Country of degree conferring institution (Overseas)
Yes
Field of Specialization
Logic, Formal Methods, Category Theory
ORCID(Open Researcher and Contributor ID)
0000-0002-0978-2200
Total Priod of education and research career in the foreign country
10years00months
Research
Current and Past Project
  • The purpose of this project is to complete the work started by Lindstrom on the expressivity of first-order logic by making his result not only syntactic-free but also semantic-free in the spirit of abstract model theory.
  • Recent developments of computer systems have triggered a paradigm shift from standard applications with fixed resources to reconfigurable systems, i.e. applications that work in different operation modes, called configurations, and react flexibly to internal and external stimuli for optimizing their performance. Very often the operation of reconfigurable systems is safety-critical: any malfunction may result in the serious injury to people. The safety requirements can be fulfilled only by applying formal methods. The purpose of this project is to provide a solid logic-based foundation for developing a formal method to describe reconfigurable systems and to reason formally about their properties. The concrete objectives are:
    O1) investigate model-theoretic properties of rather unconventional (and therefore not-well studied) logics that support the description of reconfigurable systems, and
    O2) provide proof-theoretic support for the formal verification of reconfigurable systems.
    The project will provide an original approach for the mathematical foundation of the reconfiguration such that any technology based on it will be highly adaptable and open to future improvements.
Academic Activities
Papers
1. Daniel Găină, Forcing and Calculi for Hybrid Logics, Journal of the Association for Computing Machinery, 67, 4, 2020.06, The definition of institution formalizes the intuitive notion of logic in a category-based setting. Similarly, the concept of stratified institution provides an abstract approach to Kripke semantics. This includes hybrid logics, a type of modal logics expressive enough to allow references to the nodes/states/worlds of the models regarded as relational structures, or multi-graphs. Applications of hybrid logics involve many areas of research such as computational linguistics, transition systems, knowledge representation, artificial intelligence, biomedi- cal informatics, semantic networks and ontologies. The present contribution sets a unified foundation for developing formal verification methodologies to reason about Kripke structures by defining proof calculi for a multitude of hybrid logics in the framework of stratified institutions. In order to prove completeness, the paper introduces a forcing technique for stratified institutions with nominal and frame extraction and studies a forcing property based on syntactic consistency. The proof calculus is shown to be complete and the significance of the general results is exhibited on a couple of benchmark examples of hybrid logical systems.
.
Works, Software and Database
1.
[URL].
Presentations
1. Daniel Gaina, Forcing and its applications in hybrid logics, Section of Mathematical Sciences of the Romanian Academy, the Romanian Mathematical Society, the Simion Stoilow Institute of Mathematics of the Romanian Academy, the Faculty of Mathematics and Computer Science of the University of Bucharest, 2019.07, [URL], The definition of institution formalizes the intuitive notion of logic in a category-based setting. Similarly, the concept of stratified institution provides an abstract approach to Kripke semantics. This includes hybrid logics, a type of modal logics expressive enough to allow references to the nodes/states/worlds of the models regarded as relational structures, or multi-graphs. Applications of hybrid logics involve many areas of research such as computational linguistics, transition systems, knowledge representation, artificial intelligence, biomedi- cal informatics, semantic networks and ontologies. The present contribution sets a unified foundation for developing formal verification methodologies to reason about Kripke structures by defining proof calculi for a multitude of hybrid logics in the framework of stratified institutions. In order to prove completeness, we introduce a forcing technique for stratified institutions with nominal and frame extraction and studies a forcing property based on syntactic consistency. The proof calculus is shown to be complete and the significance of the general results is exhibited on a couple of benchmark examples of hybrid logical systems..