Epistemic Runtime Verification

University of Udine

PhD Course in Computer Science and Artificial Intelligence
Cycle: 39

Runtime verification is a light weight verification technique based on the analysis of system logs. A key factor is that the internal state of the system is not observable, but partial knowledge on its behaviour may be available. The thesis will investigate the use of temporal epistemic logics (i.e. logics of knowledge and believe over time) to specify and verify hyperproperties for runtime verification. Different logical aspects, like distributed knowledge and common knowledge, and the communication between reasoning agents, will be used to model hierarchical architectures for fault detection and identification, and for prognosis. Techniques for planning in belief space will be used for the design of fault reconfiguration policies.

Are you ready to join FBK international community?

We welcome motivated applicants who are passionate about research, eager to learn, and driven by curiosity to explore new ideas.

Six reasons to become a PhD student at FBK

At FBK, our PhD program is designed to develop highly specialized researchers in a unique, stimulating environment

RESEARCH
AT FBK​

A Hub of innovation and collaboration​

TOWARD PHD EXCELLENCE

FBK stands out as one of Italy’s leading research institutions

international
network

National and international
companies and universities

learning opportunities

Explore a world of learning
at FBK

Discover Trento

One of the most Italy’s
livable city

Join FBK

A truly international
community