|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.
Reseacher Profiling Tool Kyushu University Pure
PhD in information science from Japan Advanced Institute of Science and Technology
Country of degree conferring institution (Overseas)
Field of Specialization
Logic, Formal Methods, Category Theory
ORCID(Open Researcher and Contributor ID)
Total Priod of education and research career in the foreign country
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.
Works, Software and Database
|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..|