| Daniel Mircea GAINA | Last modified date：2023.11.22 |
Associate Professor /
Institute of Mathematics for Industry
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.elsevierpure.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, Master's degree in algebraic specification from Normal Superior School of Bucharest, Master's degree in fundamentals of informatics from University of Bucharest, BSc in informatics from University of Bucharest
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
Outline Activities
My research is focused on algebraic specification, one of the most promising aproach to formal methods assisting the developing of software systems at several stages such as design, specification and formal verification. Algebraic specification and programming languages are rigorously based on logic, which amounts to the existence of a logical system underlying the language such that each language feature and construction can be expressed as a mathematical entity of the underlying logic.
Research
Research Interests
Membership in Academic Society
- Reconfigurable systems are found everywhere: software-driven medical devices (such as infusion pumps, pacemakers, imaging machines and pill cameras), intelligent transportation systems, cars, or mobile robots. They all interact with their users and the environment in which they operate. Reconfigurable systems are often used in safety-critical areas where any malfunction may cause serious injuries to human beings. The safety requirements can be fulfilled only by applying formal methods. The objective is to develop a software tool for the formal specification and verification of reconfigurable systems.
keyword : theorem proving, reconfiguration paradigm, hybrid systems, verification methodology
2023.04～2026.04. - 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 is to provide a solid logic-based foundation for developing a formal method to describe reconfigurable systems and to reason formally about their properties.
keyword : reconfigurable systems, formal methods, hybrid-dynamic logics
2020.04～2023.04.
- 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.
Papers
| 1. | Daniel Găină, Forcing and Calculi for Hybrid Logics, Journal of the Association for Computing Machinery, https://doi.org/10.1145/3400294, 67, 4, 1-55, 2020.06, [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, 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..  |
Presentations
| 1. | Daniel Găină, 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.. |
- Mathematical Society of Japan
Educational
Educational Activities
I have taught a variety of applied mathematical subjects such as algebraic specification, model theoretic topics for the design of specification and verification languages, or term rewriting. I organize lectures in collaboration with other universities such as La Trobe University. I also supervise graduate research students.
Social
Professional and Outreach Activities
I am involved in research collaborations with European and Australian academics as well as with Japanese researchers.
I organize an online seminar for the development of a software tool for the specification and verification of reconfigurable systems. My collaborators for this project are Adrian Riesco (Complutense University of Madrid) and Ionut Tutu (Institute of Mathematics of the Romanian Academy).
I work with Tomasz Kowalski (Jagiellonian University, Poland) and Guillermo Badia (The University of Queensland) on a project where we study the relationship between gaining expressive power in extending first-order logics and losing 'control' over the extension.
I am involved in the organization of joint research seminars with Mathematics and Statistics Department of La Trobe University. .
I organize an online seminar for the development of a software tool for the specification and verification of reconfigurable systems. My collaborators for this project are Adrian Riesco (Complutense University of Madrid) and Ionut Tutu (Institute of Mathematics of the Romanian Academy).
I work with Tomasz Kowalski (Jagiellonian University, Poland) and Guillermo Badia (The University of Queensland) on a project where we study the relationship between gaining expressive power in extending first-order logics and losing 'control' over the extension.
I am involved in the organization of joint research seminars with Mathematics and Statistics Department of La Trobe University. .
Unauthorized reprint of the contents of this database is prohibited.