A5087985917- Logic, Reasoning, and Knowledge
- Formal Methods in Verification
- Constraint Satisfaction and Optimization
- Logic, programming, and type systems
- Semantic Web and Ontologies
- Petri Nets in System Modeling
- Advanced Algebra and Logic
- Software Testing and Debugging Techniques
- Model-Driven Software Engineering Techniques
- Advanced Control Systems Optimization
- Control Systems and Identification
- semigroups and automata theory
- Service-Oriented Architecture and Web Services
- Advanced Database Systems and Queries
- Artificial Intelligence in Games
- Advanced Optimization Algorithms Research
- Natural Language Processing Techniques
- Business Process Modeling and Analysis
- Embedded Systems Design Techniques
- Manufacturing Process and Optimization
- Advanced Malware Detection Techniques
- Real-Time Systems Scheduling
- Distributed systems and fault tolerance
- Machine Learning and Algorithms
- Probabilistic and Robust Engineering Design
University of Padua
2017-2024
Universidad de Málaga
2018
University of Ferrara
2018
University of Bologna
2014-2016
Istituto Nazionale di Fisica Nucleare, Sezione di Trieste
2016
University of Verona
2007-2014
University of Udine
2004-2007
Ca' Foscari University of Venice
2000
We introduce a platform-based design methodology that uses contracts to specify and abstract the components of cyber-physical system (CPS), provide formal support entire CPS flow. The is carried out as sequence refinement steps from high-level specification an implementation built library at lower level. review formalisms tools can be used specify, analyze, or synthesize different levels abstraction. For each level, we highlight how contract operations concretely computed well research...
SUMMARY In many applicative fields, there is the need to model and design complex systems having a mixed discrete continuous behavior that cannot be characterized faithfully using either or models only. Such consist of control part operates in environment are named hybrid because their nature. Unfortunately, most verification problems for systems, like reachability analysis, turn out undecidable. Because this, approximation techniques tools estimate reachable set have been proposed...
Journal Article Tableaux for Logics of Subinterval Structures over Dense Orderings Get access Davide Bresolin, Bresolin Department Computer Science, University Verona, ItalyE-mail: bresolin@sci.univr.it Search other works by this author on: Oxford Academic Google Scholar Valentin Goranko, Goranko Informatics and Mathematical Modelling, Technical DenmarkE-mail: vfgo@imm.dtu.dk Angelo Montanari, Montanari Mathematics Udine, angelo.montanari@dimi.uniud.it; pietro.sala@dimi.uniud.it Pietro Sala...
The introduction of Halpern and Shoham's modal logic intervals (later on called HS) dates back to 1986. Despite its natural semantics, this is undecidable over all interesting classes temporal structures. This discouraged research in area until recently, when a number non trivial decidable fragments have been found. paper contribution toward the complete classification HS fragments. Different combinations Allen's interval relations begins (B), meets (A), later (L), their inverses A̅, B̅, L̅,...
We investigate the satisfiability problem for Horn fragments of Halpern-Shoham interval temporal logic depending on type (box or diamond) modal operators, underlying linear order (discrete dense), and semantics relations (reflexive irreflexive). For example, we show that formulas with diamonds is undecidable any orders semantics. On contrary, boxes tractable over both discrete dense under reflexive irreflexive but becomes Satisfiability binary always
In this article, we discuss formal methods for the verification of properties control systems designed autonomous robotic systems. last few decades, robotics played a relevant role in progress surgery. The use robots operating rooms has given rise to new terminologies: robot-assisted surgery, medical robotics, rehabilitation telesurgery, assistive systems, and so on. Since surgery is relatively field investigation, there are no established bringing concepts operational procedures surgical...
There has been a growing interest in defining models of automata enriched with time. For instance, timed were introduced as extended clocks. In this paper, we study finite state machines (TFSMs), i.e., FSMs time, which accept input words and generate output words. Here discuss some TFSMs single clock: guards, timeouts, both guards timeouts. We solve the problem equivalence checking for all three models, compare their expressive power, characterizing subclasses timeouts that are equivalent to...
Unlike the Moon, dark side of interval temporal logics is one we usually see: their ubiquitous undesirability. Identifying minimal undecidable thus a natural and important issue in research agenda area. The decidability status logic often depends on class models (in our case, structures)in which it interpreted. In this paper, have identified several new amongst fragments Halpern-Shoham HS, including overlaps relation, over classes all finite linear orders, as well meet subinterval relations,...
The relevance of formal verification methods is widely recognized in the computer science and embedded systems community. Recently, such have been introduced also within control community, to help designers developing architectures for complex robotics systems. Robotic typically mix continuous discrete behaviors that cannot be modeled faithfully using neither continuous-only nor discrete-only formalisms. interaction dynamics makes treatment this kind computationally very demanding, justifies...
Temporal reasoning plays an important role in artificial intelligence. logics provide a natural framework for its formalization and implementation. A standard way of enhancing the expressive power temporal is to replace their unidimensional domain by multidimensional one. In particular, such dimensional increase can be exploited obtain spatial counterparts logics. Unfortunately, it often involves blow up complexity, possibly losing decidability. this paper, we propose generalization...