Abstract
It can be desirable to specify polices that require a system to achieve some outcome even if a certain number of failures occur. This paper proposes a logic, RoCTL*, which extends CTL* with operators from Deontic logic, and a novel operator referred to as “Robustly”. This novel operator acts as variety of path quantifier allowing us to consider paths which deviate from the desired behaviour of the system. Unlike most path quantifiers, the Robustly operator must be evaluated over a path rather than just a state; the Robustly operator quantifies over paths produced from the current path by altering a single step. The Robustly operator roughly represents the phrase “even if an additional failure occurs now or in the future”. This paper examines the expressivity of this new logic, motivates its use and shows that it is decidable.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Emerson, E.A., Sistla, A.P.: Deciding full branching time logic. Technical report, University of Texas at Austin, Austin, TX, USA (1985)
Clarke, E., Emerson, E.: Synthesis of synchronization skeletons for branching time temporal logic. In: Proc. IBM Workshop on Log. of Progr., Yorktown Heights, pp. 52–71. Springer, Heidelberg (1981)
French, T., McCabe-Dansted, J.C., Reynolds, M.: A temporal logic of robustness, RoCTL*. Technical report, UWA (2007) http://dansted.org/RoCTL07.pdf
Forrester, J.W.: Gentle murder, or the adverbial samaritan. J. Philos. 81(4), 193–197 (1984)
van der Torre, L.W.N., Tan, Y.: The temporal analysis of Chisholm’s paradox. In: Senator, T., Buchanan, B. (eds.) Proc. 14th Nation. Conf. on AI and 9th Innov. Applic. of AI Conf., Menlo Park, California, pp. 650–655. AAAI Press, Stanford, California (1998)
McCarty, L.T.: Defeasible deontic reasoning. Fundam. Inform. 21(1/2), 125–148 (1994)
Belnap, N.: Backwards and forwards in the modal logic of agency. Philos. Phenomen. Res. 51(4), 777–807 (1991)
de Weerdt, M., Bos, A., Tonino, H., Witteveen, C.: A resource logic for multi-agent plan merging. Annals of Math. and AI 37(1-2), 93–130 (2003)
Broersen, J., Dignum, F., Dignum, V., Meyer, J.J.C.: In: Designing a Deontic Logic of Deadlines. In: Lomuscio, A.R., Nute, D. (eds.) DEON 2004. LNCS (LNAI), vol. 3065, pp. 43–56. Springer, Heidelberg (2004)
Long, W., Sato, Y., Horigome, M.: Quantification of sequential failure logic for fault tree analysis. Reliab. Eng. Syst. Safe. 67, 269–274 (2000)
Hansson, H., Jonsson, B.: A logic for reasoning about time and reliability. Form. Asp. Comput. 6(5), 512–535 (1994)
Aldewereld, H., Grossi, D., Vazquez-Salceda, J., Dignum, F.: Designing normative behaviour by the use of landmarks. In: Agents, Norms and Institutions for Regulated Multiag. Syst., Utrecht, The Netherlands (2005)
Rodrigo, A., Eduardo, A.: Normative pragmatics for agent communication languages. In: Akoka, J., Liddle, S.W., Song, I.-Y., Bertolotto, M., Comyn-Wattiau, I., van den Heuvel, W.-J., Kolp, M., Trujillo, J., Kop, C., Mayr, H.C. (eds.) Perspectives in Conceptual Modeling. LNCS, vol. 3770, pp. 172–181. Springer, Heidelberg (2005)
Jéron, T., Marchand, H., Pinchinat, S., Cordier, M.O.: Supervision patterns in discrete event systems diagnosis. In: 8th Internat. Workshop on Discrete Event Syst., pp. 262–268 (2006)
Arnold, A., Vincent, A., Walukiewicz, I.: Games for synthesis of controllers with partial observation. TCS 303(1), 7–34 (2003)
Reynolds, M.: An axiomatization of full computation tree logic. J. Symb. Log. 66(3), 1011–1057 (2001)
Emerson, E.A.: Alternative semantics for temporal logics. TCS 26, 121–130 (1983)
Kupferman, O.: Augmenting branching temporal logics with existential quantification over atomic propositions. In: Comput. Aid. Verfic., Proc. 7th Int. Conf., Liege, pp. 325–338. Springer, Heidelberg (1995)
Emerson, E.A., Sistla, A.P.: Deciding branching time logic. In: STOC 1984: Proc. 16th annual ACM sympos. on Theory of computing, New York, NY, USA, pp. 14–24. ACM Press, New York (1984)
French, T.: Decidability of quantifed propositional branching time logics. In: AI 2001. Proc. 14th Austral. Joint Conf. on AI, London, UK, pp. 165–176. Springer, Heidelberg (2001)
Sistla, A.P., Vardi, M.Y., Wolper, P.: The complementation problem for buc̈hi automata with applications to temporal logic. TCS 49(2-3), 217–237 (1987)
French, T.: Bisimulation Quantifiers for Modal Logics. PhD thesis, UWA (2006)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2007 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
French, T., Mc Cabe-Dansted, J.C., Reynolds, M. (2007). A Temporal Logic of Robustness. In: Konev, B., Wolter, F. (eds) Frontiers of Combining Systems. FroCoS 2007. Lecture Notes in Computer Science(), vol 4720. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-74621-8_13
Download citation
DOI: https://doi.org/10.1007/978-3-540-74621-8_13
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-74620-1
Online ISBN: 978-3-540-74621-8
eBook Packages: Computer ScienceComputer Science (R0)