UCL Discovery
UCL home » Library Services » Electronic resources » UCL Discovery

Soft component automata: Composition, compilation, logic, and verification

Kappé, T; Lion, B; Arbab, F; Talcott, C; (2019) Soft component automata: Composition, compilation, logic, and verification. Science of Computer Programming , 183 , Article 102300. 10.1016/j.scico.2019.08.001.

[img] Text
main.pdf - Accepted version
Access restricted to UCL open access staff until 17 August 2020.

Download (544kB)

Abstract

The design of a complex system warrants a compositional methodology, i.e., composing simple components to obtain a system that meaningfully exhibits their collective behavior. We propose an automaton-based paradigm for compositional design of such systems where an action is accompanied by one or more preferences. At run-time, these preferences provide a natural fallback mechanism for the component, while at design-time they can be used to reason about the behavior of the component in an uncertain physical world. Using algebraic structures on preferences and actions, we can compose formal representations of individual components or agents to obtain a representation of the composed system, exhibiting intuitively meaningful behavior. We extend linear temporal logic with two unary connectives that reflect the compositional structure of actions, and show that it is decidable whether all behaviors of a given automaton satisfy a formula of this extended logic. We then show how this logic can be used to diagnose undesired behavior by tracing the falsification of a specification back to one or more culpable components. Lastly, we implement a toolchain that compiles our automata to Maude, allowing us to apply the rich model checking capability of Maude to verify agent behavior.

Type: Article
Title: Soft component automata: Composition, compilation, logic, and verification
DOI: 10.1016/j.scico.2019.08.001
Publisher version: https://doi.org/10.1016/j.scico.2019.08.001
Language: English
Additional information: This version is the author accepted manuscript. For information on re-use, please refer to the publisher’s terms and conditions.
Keywords: Compositionality, Diagnosis, Soft preference, Compilation, Verification
UCL classification: UCL
UCL > Provost and Vice Provost Offices
UCL > Provost and Vice Provost Offices > UCL BEAMS
UCL > Provost and Vice Provost Offices > UCL BEAMS > Faculty of Engineering Science
URI: https://discovery.ucl.ac.uk/id/eprint/10081003
Downloads since deposit
0Downloads
Download activity - last month
Download activity - last 12 months
Downloads by country - last 12 months

Archive Staff Only

View Item View Item