Abstract
The design of a complex system warrants a compositional methodology, i.e., composing simple components to obtain a larger system that exhibits their collective behavior in a meaningful way. 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 structures that tell us how to compose preferences and actions, we can compose formal representations of individual components or agents to obtain a representation of the composed system. We extend Linear Temporal Logic with two unary connectives that reflect the compositional structure of the actions, and show how it can be used to diagnose undesired behavior by tracing the falsification of a specification back to one or more culpable components.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
Notes
- 1.
Here, we use the abbreviation SCA exclusively to refer to Soft Component Automata.
- 2.
This is a rather simplistic description of energy management. We remark that a more detailed description is possible by extending SCAs with memory cells [15] and using a memory cell to store the energy level. In such a setup, a state would represent a range of energy values that determines the components disposition regarding resources.
- 3.
A more detailed description of such a component could count the number of times the drone has moved without taking a snapshot first, and assign the preference of doing so again accordingly.
- 4.
Recall that \(\mathsf {move}_2\) is the composition of \(\mathsf {move}\) and \(\mathsf {discharge}_2\), i.e., \(\mathsf {move}\sqsubseteq \mathsf {move}_2\).
- 5.
Recall that \(7 \le _{\mathbb {W}} 5\), so 5 is a “higher” threshold in this context.
- 6.
Arguably, \(A_\mathsf {e}\) as a whole may not be responsible, because modifying the preference of the \(\mathsf {move}\)-loop on \(q_N\) in \(A_\mathsf {s}\) can help to exclude the undesired behavior as well. In our framework, however, the threshold is a generic property of any SCA, and so we use it as a handle for talking about localizing undesired behaviors to component SCAs.
References
Arbab, F., Santini, F.: Preference and similarity-based behavioral discovery of services. In: ter Beek, M.H., Lohmann, N. (eds.) WS-FM 2012. LNCS, vol. 7843, pp. 118–133. Springer, Heidelberg (2013). doi:10.1007/978-3-642-38230-7_8
Baier, C., Blechmann, T., Klein, J., Klüppelholz, S., Leister, W.: Design and verification of systems with exogenous coordination using vereofy. In: Margaria, T., Steffen, B. (eds.) ISoLA 2010. LNCS, vol. 6416, pp. 97–111. Springer, Heidelberg (2010). doi:10.1007/978-3-642-16561-0_15
Baier, C., Sirjani, M., Arbab, F., Rutten, J.: Modeling component connectors in Reo by constraint automata. Sci. Comput. Program. 61, 75–113 (2006)
Bistarelli, S. (ed.): Semirings for Soft Constraint Solving and Programming. LNCS, vol. 2962. Springer, Heidelberg (2004). doi:10.1007/b95712
Bistarelli, S., Montanari, U., Rossi, F.: Constraint solving over semirings. In: Proceedings of the International Joint Conference on Artificial Intelligence (IJCAI), pp. 624–630 (1995)
Bistarelli, S., Montanari, U., Rossi, F.: Semiring-based constraint satisfaction and optimization. J. ACM 44(2), 201–236 (1997)
Büchi, J.R.: On a decision method in restricted second order arithmetic. In: Proceedings of Logic, Methodology and Philosophy of Science, pp. 1–11. Stanford University Press, Stanford (1962)
Casanova, P., Garlan, D., Schmerl, B.R., Abreu, R.: Diagnosing unobserved components in self-adaptive systems. In: Proceedings of Software Engineering for Adaptive and Self-Managing Systems (SEAMS), pp. 75–84 (2014)
Debouk, R., Lafortune, S., Teneketzis, D.: Coordinated decentralized protocols for failure diagnosis of discrete event systems. Discrete Event Dyn. Syst. 10(1–2), 33–86 (2000)
Gadducci, F., Hölzl, M., Monreale, G.V., Wirsing, M.: Soft constraints for lexicographic orders. In: Castro, F., Gelbukh, A., González, M. (eds.) MICAI 2013. LNCS, vol. 8265, pp. 68–79. Springer, Heidelberg (2013). doi:10.1007/978-3-642-45114-0_6
Goessler, G., Astefanoaei, L.: Blaming in component-based real-time systems. In: Proceedings of Embedded Software (EMSOFT), pp. 7:1–7:10 (2014)
Gössler, G., Stefani, J.-B.: Fault ascription in concurrent systems. In: Ganty, P., Loreti, M. (eds.) TGC 2015. LNCS, vol. 9533, pp. 79–94. Springer, Cham (2016). doi:10.1007/978-3-319-28766-9_6
Hölzl, M.M., Meier, M., Wirsing, M.: Which soft constraints do you prefer? Electr. Notes Theor. Comput. Sci. 238(3), 189–205 (2009)
Hüttel, H., Larsen, K.G.: The use of static constructs in a model process logic. In: Meyer, A.R., Taitslin, M.A. (eds.) Logic at Botik 1989. LNCS, vol. 363, pp. 163–180. Springer, Heidelberg (1989). doi:10.1007/3-540-51237-3_14
Jongmans, S.T., Kappé, T., Arbab, F.: Constraint automata with memory cells and their composition. Sci. Comput. Program. 146, 50–86 (2017)
Kappé, T.: Logic for Soft Component Automata. Master’s thesis, Leiden University, Leiden, The Netherlands (2016). http://liacs.leidenuniv.nl/assets/Masterscripties/CS-studiejaar-2015-2016/Tobias-Kappe.pdf
Kappé, T., Arbab, F., Talcott, C.: A component-oriented framework for autonomous agents (2017). https://arxiv.org/abs/1708.00072
Kappé, T., Arbab, F., Talcott, C.L.: A compositional framework for preference-aware agents. In: Proceedings of Workshop on Verification and Validation of Cyber-Physical Systems (V2CPS), pp. 21–35 (2016)
Koehler, C., Clarke, D.: Decomposing port automata. In: Proceedings ACM Symposium on Applied Computing (SAC), pp. 1369–1373 (2009)
Mason, I.A., Nigam, V., Talcott, C., Brito, A.: A framework for analyzing adaptive autonomous aerial vehicles. In: Proceedings of Workshop on Formal Co-Simulation of Cyber-Physical Systems (CoSim) (2017)
Muller, D.E., Saoudi, A., Schupp, P.E.: Weak alternating automata give a simple explanation of why most temporal and dynamic logics are decidable in exponential time. In: Proceedings of Symposium on Logic in Computer Science (LICS), pp. 422–427 (1988)
Neidig, J., Lunze, J.: Decentralised Diagnosis of Automata Networks. IFAC Proceedings Volumes, vol. 38(1), pp. 400–405 (2005)
Rutten, J.J.M.M.: A coinductive calculus of streams. Math. Struct. Comput. Sci. 15(1), 93–147 (2005)
Sampath, M., Sengupta, R., Lafortune, S., Sinnamohideen, K., Teneketzis, D.: Failure diagnosis using discrete-event models. IEEE Trans. Contr. Sys. Techn. 4(2), 105–124 (1996)
Talcott, C.L., Arbab, F., Yadav, M.: Soft agents: exploring soft constraints to model robust adaptive distributed cyber-physical agent systems. In: Software, Services, and Systems – Essays Dedicated to Martin Wirsing on the Occasion of His Retirement from the Chair of Programming and Software Engineering, pp. 273–290 (2015)
Talcott, C., Nigam, V., Arbab, F., Kappé, T.: Formal specification and analysis of robust adaptive distributed cyber-physical systems. In: Bernardo, M., De Nicola, R., Hillston, J. (eds.) SFM 2016. LNCS, vol. 9700, pp. 1–35. Springer, Cham (2016). doi:10.1007/978-3-319-34096-8_1
Vardi, M.Y.: An automata-theoretic approach to linear temporal logic. In: Moller, F., Birtwistle, G. (eds.) Logics for Concurrency. LNCS, vol. 1043, pp. 238–266. Springer, Heidelberg (1996). doi:10.1007/3-540-60915-6_6
Wirsing, M., Denker, G., Talcott, C.L., Poggio, A., Briesemeister, L.: A rewriting logic framework for soft constraints. Electr. Notes Theor. Comput. Sci. 176(4), 181–197 (2007)
Acknowledgements
The authors would like to thank Vivek Nigam and the anonymous FACS-referees for their valuable feedback. This work was partially supported by ONR grant N00014–15–1–2202.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2017 Springer International Publishing AG
About this paper
Cite this paper
Kappé, T., Arbab, F., Talcott, C. (2017). A Component-Oriented Framework for Autonomous Agents. In: Proença, J., Lumpe, M. (eds) Formal Aspects of Component Software. FACS 2017. Lecture Notes in Computer Science(), vol 10487. Springer, Cham. https://doi.org/10.1007/978-3-319-68034-7_2
Download citation
DOI: https://doi.org/10.1007/978-3-319-68034-7_2
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-68033-0
Online ISBN: 978-3-319-68034-7
eBook Packages: Computer ScienceComputer Science (R0)