Daniel Mircea GAINA | Last modified date：2020.11.12 |

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

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

**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, 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.. |

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), Ionut Tutu (Institute of Mathematics of the Romanian Academy), and Claudia Chirita (University of Dundee).

I work with Tomasz Kowalski (La Trobe University) 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 recently started a collaboration with a software company with the purpose of finding mathematical solutions to software problems in industry..

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), Ionut Tutu (Institute of Mathematics of the Romanian Academy), and Claudia Chirita (University of Dundee).

I work with Tomasz Kowalski (La Trobe University) 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 recently started a collaboration with a software company with the purpose of finding mathematical solutions to software problems in industry..

Unauthorized reprint of the contents of this database is prohibited.