The general aim of my research is to introduce comprehensive
logical systems that automatically exploit peculiarities of the
problems under consideration,
and to show that such logical systems can indeed achieve
a significant speedup over the traditional ones.
In particular, I am looking for:
Effective logical formalisms for
resource- and memory-sensitive reasoning
(linear logic, separation logic, and the like)
Effective logical formalisms to specify and to investigate
real-time and hybrid systems with quantitative time
constraints.
The aim is to develop efficient and comprehensive logical systems
and programming tools capable of handling
important properties of real-time dynamic systems
such as safety, liveness, schedulability, surviveness, simulation,
monitoring, etc.
Effective logical formalisms to specify and investigate security
problems in multi-agent systems.
The aim is to develop efficient logical systems capable of handling
security protocols in software, distributed systems, and
concurrent systems.
Effective logical formalisms for assured information sharing.
The aim is to develop methods and algorithms to enable multiple
parties to share information and at the same time enforce
confidentiality, privacy, trust, release, dissemination,
data quality and provenance policies.
Effective logical formalisms for AI systems.
We are looking for the comprehensive semantics and planning algorithms
for robot systems under stochastic and uncertain conditions,
for which the planning problem becomes the winning strategies problem.
Effective logical formalisms for Computational Linguistics.
The aim of this research is to develop comprehensive and efficient
logical formalisms capable of handling syntactical and semantical
properties of a natural language.
Natural characterizations of virtually all major complexity classes
in terms of expressibility within natural fragments of linear logic
and its generalizations.
In turn, this provides an opportunity to analyze complexity classes,
their strengths and limitations, by studying the expressive power
of linear logic, light linear logic,
elementary linear logic, and their Horn and disjunctive Horn
fragments.
Bridging Logic and Combinatorics.
The aim of this research is to create direct bridges between
techniques from the formal logic world and
specific mathematical problems
studied completely independently in the world of combinatorics,
and to show
how techniques from one field can sometimes be useful in another.