Search
Now showing items 1-7 of 7
A PO Characterisation of Reconfiguration
(2022)
We consider partial order semantics of concurrent systems in which local reconfigurations may have global side effects. That is, local changes happening to an entity may block or unblock events relating to others, namely, ...
Incorporating Monitors in Reactive Synthesis without Paying the Price
(19th International Symposium on Automated Technology for Verification and Analysis, 2021)
Temporal synthesis attempts to construct reactive programs
that satisfy a given declarative (LTL) formula. Practitioners have found
it challenging to work exclusively with declarative speci cations, and
have found ...
Actions over Core-closed Knowledge Bases
(2022)
We present new results on the application of semantic- and knowledge-based reasoning techniques to the analysis of cloud deployments. In particular, to the security of Infrastructure as Code configuration files, encoded ...
Model Checking Reconfigurable Interacting Systems
(International Symposium on Leveraging Applications of Formal Methods, 2022)
Reconfigurable multi-agent systems consist of a set of autonomous agents, with integrated interaction capabilities that feature opportunistic interaction. Agents seemingly reconfigure their interactions interfaces by forming ...
Runtime Verification meets Controller Synthesis
(2022)
Reactive synthesis guarantees correct-by-construction controllers from logical specifications, but is costly—2EXPTIME-complete in the size of the specification. In a practical setting, the desired controllers need to ...
A Survey on Satisfiability Checking for the μ -Calculus Through Tree Automata
(2022)
Algorithms for model checking and satisfiability of the modal μ -calculus start by converting formulas to alternating parity tree automata. Thus, model checking is reduced to checking acceptance by tree automata and ...
R-CHECK: A Model Checker for Verifying Reconfigurable MAS
(AAMAS 2022, 2022)
Reconfigurable multi-agent systems consist of a set of autonomous
agents, with integrated interaction capabilities that feature opportunistic
interaction. Agents seemingly reconfigure their interactions
interfaces by ...