%0 Conference Proceedings
%T Logics for Petri Nets with Propagating Failures
%+ High-Assurance Software Laboratory [Braga, Portugal] ( HASLab )
%+ Center for Research & Development in Mathematics and Applications [Aveiro] (CIDMA)
%+ Departamento de Ciência Da Computação [Rio de Janeiro] (DCC)
%A Gomes, Leandro
%A Madeira, Alexandre
%A Benevides, Mario
%Z Part 4: Verification
%< avec comité de lecture
%( Lecture Notes in Computer Science
%B 8th International Conference on Fundamentals of Software Engineering (FSEN)
%C Tehran, Iran
%Y Hossein Hojjat
%Y Mieke Massink
%I Springer International Publishing
%3 Fundamentals of Software Engineering
%V LNCS-11761
%P 145-157
%8 2019-05-01
%D 2019
%R 10.1007/978-3-030-31517-7_10
%Z Computer Science [cs]Conference papers
%X Petri nets play a central role in the formal modelling of a wide range of complex systems and scenarios. Their ability to handle with both concurrency and resource awareness justifies their spread in the current formal development practices. On the logic side, Dynamic Logics are widely accepted as the de facto formalisms to reason about computational systems. However, as usual, the application to new situations raises new challenges and issues.The ubiquity of failures in the execution of current systems, interpreted in these models as triggered events that are not followed by the corresponding transition, entails not only the adjustment of these structures to deal with this reality, but also the introduction of new logics adequate to this emerging phenomenon.This paper contributes to this challenge by exploring a combination of two previous works of the authors, namely the Propositional Dynamic Logic for Petri Nets [1] and a parametric construction of multi-valued dynamic logics presented in [13]. This exercise results in a new family of Dynamic Logics for Petri Nets suitable to deal with firing failures.
%G English
%Z TC 2
%Z WG 2.2
%2 https://inria.hal.science/hal-03769133/document
%2 https://inria.hal.science/hal-03769133/file/490001_1_En_10_Chapter.pdf
%L hal-03769133
%U https://inria.hal.science/hal-03769133
%~ IFIP-LNCS
%~ IFIP
%~ IFIP-TC
%~ IFIP-TC2
%~ IFIP-WG2-2
%~ IFIP-FSEN
%~ IFIP-LNCS-11761