A5021825279- Japanese History and Culture
- Formal Methods in Verification
- Advanced Database Systems and Queries
- Chinese history and philosophy
- Gene Regulatory Network Analysis
- Data Management and Algorithms
- Semantic Web and Ontologies
- Simulation Techniques and Applications
- Bayesian Modeling and Causal Inference
- Model-Driven Software Engineering Techniques
- Religious Tourism and Spaces
- Logic, Reasoning, and Knowledge
- Distributed systems and fault tolerance
- Receptor Mechanisms and Signaling
- Natural Language Processing Techniques
- Advanced Software Engineering Methodologies
- Machine Learning and Algorithms
- Anomaly Detection Techniques and Applications
- Artificial Immune Systems Applications
- Neuroscience and Neural Engineering
- Time Series Analysis and Forecasting
- Philippine History and Culture
- Constraint Satisfaction and Optimization
- Data Visualization and Analytics
- Travel Writing and Literature
University of Trieste
2015-2025
TU Wien
2017-2022
University of Tennessee at Knoxville
2011-2019
Istituto di Scienza e Tecnologie dell'Informazione "Alessandro Faedo"
2015
IMT School for Advanced Studies Lucca
2013-2015
Saarland University
2015
University of California, Santa Barbara
2003
Cyber-Physical Systems~(CPS) consist of collaborative, networked and tightly intertwined computational (logical) physical components, each operating at different spatial temporal scales. Hence, the requirements play an essential role for their correct safe execution. Furthermore, local interactions among system components result in global spatio-temporal emergent behaviors often impossible to predict design time. In this work, we pursue a complementary approach by introducing STREL novel...
Stochastic models such as Continuous-Time Markov Chains (CTMC) and Hybrid Automata (SHA) are powerful formalisms to model reason about the dynamics of biological systems, due their ability capture stochasticity inherent in processes. A classical question formal modelling with clear relevance is checking problem. i.e. calculate probability that a behaviour, expressed for instance terms certain temporal logic formula, may occur given stochastic process. However, one not only be interested...
We present an extension of the linear time, time-bounded, Signal Temporal Logic to describe spatio-temporal properties. consider a discrete location/ patch-based representation space, with population interacting agents evolving in each location and migrating from one patch
From smart buildings to medical devices nations, software systems increasingly integrate computation, networking, and interaction with the physical environment. These are known as Cyber-Physical Systems (CPS). While these open new opportunities deliver improved quality of life for people reinvigorate computing, their engineering is a difficult problem given level heterogeneity dynamism they exhibit. progress has been made, we argue that complexity now at such existing approaches need major...
Application development for the modern Web involves sophisticated engineering workflows – including user interface (UI) aspects. Such interfaces comprise elements that are typically created with HTML/CSS markup and JavaScript-like languages, yielding documents. Their testing entails performing checks to examine visual structural parts of resulting UI software against requirements such as usability, accessibility, performance, or, increasingly, compliance standards. However, current...
Internet of things systems are increasingly common nowadays. They feature spatially-distributed, mobile entities with an arising collective behavior. Such bear radionavigation sensors that produce positioning information, then used by the (software-enabled) device to information over time, referred as trajectories. However, software applications built on top this require composite models space be in place; such can provide adaptive behaviors observing, evaluating, and reacting a constantly...
In the Edo period (1600-1868), status- and gender-based expectations largely defined a person's place identity in society. The wayfarers of time, however, discovered that travel provided opportunity to escape from confines everyday. Cultured travelers seventeenth eighteenth centuries wrote memoirs celebrate their profession as belle-lettrists. For women particular open road blank page diary offered precious create personal hierarchies less by gender more culture refinement.After...
"Mapping Early Modern Japan: Space, Place, and Culture in the Tokugawa Period (1603–1868)." History: Reviews of New Books, 31(4), pp. 174–175
In spatially located, large scale systems, time and space dynamics interact drives the behaviour. Examples of such systems can be found in many smart city applications Cyber-Physical Systems. this paper we present Signal Spatio-Temporal Logic (SSTL), a modal logic that used to specify spatio-temporal properties linear discrete models. The is equipped with Boolean quantitative semantics for which efficient monitoring algorithms have been developed. As such, it suitable real-time verification...
Traffic systems, where human and autonomous drivers interact, are a very relevant instance of complex systems produce behaviors that can be regarded as trajectories over time. Their monitoring achieved by means carefully stated properties describing the expected behavior. Such expressed using Signal Temporal Logic (STL), specification language for expressing temporal in formal human-readable way. However, manually authoring these is hard task, since it requires mastering knowing system to...
Abstract Describing the properties of complex systems that evolve over time is a crucial requirement for monitoring and understanding them. Signal Temporal Logic (STL) framework proved to be effective this aim because it expressive allows state as human-readable formulae. Crafting STL formulae fit particular system is, however, difficult task. For reason, few approaches have been proposed recently automatic learning starting from observations system. In paper, we propose BUSTLE (Bi-level...
This report presents the results from falsification category of 2024 competition in Applied Verification for Continuous and Hybrid Systems (ARCH) workshop. The summarizes rules settings, benchmark models tool comparison, provides background on participating teams tools. Finally, it discusses competition.