LTL-Constrained Steady-State Policy Synthesis

Decision-making policies for agents are often synthesized with the constraint that a formal specification of behaviour is satisfied. Here we focus on infinite-horizon properties. On the one hand, Linear Temporal Logic (LTL) is a popular example of a formalism for qualitative specifications. On the other hand, Steady-State Policy Synthesis (SSPS) has recently received considerable attention as it provides a more quantitative and more behavioural perspective on specifications, in terms of the frequency with which states are visited. Finally, rewards provide a classic framework for quantitative properties. In this paper, we study Markov decision processes (MDP) with the specification combining all these three types. The derived policy maximizes the reward among all policies ensuring the LTL specification with the given probability and adhering to the steady-state constraints. To this end, we provide a unified solution reducing the multi-type specification to a multi-dimensional long-run average reward. This is enabled by Limit-Deterministic Büchi Automata (LDBA), recently studied in the context of LTL model checking on MDP, and allows for an elegant solution through a simple linear programme. The algorithm also extends to the general omega-regular properties and runs in time polynomial in the sizes of the MDP as well as the LDBA.

Modeling security properties of authentication of cryptographic protocols using spin formal verification

To assess the quality and security of cryptographic protocols, we use various formal verification tools, such as Scyther tool, Avispa, ProVerif. these formal verifiers can check the protocol for vulnerability to attacks on secrecy and authentication, as these are the most prevalent attacks on protocols. However, this is not enough to fully analyze the security of the protocol. In this article, we will use linear temporal logic (LTL) model checking with SPIN. This tool, unlike the formal verifiers listed above, is not designed for a specific application in the context of cryptographic protocols; however, it has a very wide range of possibilities. In particular, for each security property, it is possible to describe the behavior of an attacker and test for the stability of the protocol model to its various attacks. The purpose of this work is to describe the developed methodology for verifying the security of authentication properties using the SPIN verifier.

SE-LTL Model-checking on Timed GRAFCETS via ε-TPN

The GRAFCET standard (IEC 60848) is one of the convenient formalisms used to specify the behaviour of the automated systems. Being just a semi-formal language, the usual practice is to go through an unambiguous formalism such as time Petri net (TPN) in order to validate a specification expressed by a GRAFCET model. In this paper, we propose how to perform model-checking on a GRAFCET model translated into a ε-TPN, specifically with State-Event Linear Temporal Logic (SE-LTL). Especially, we provide a way to take into account quantitative time constraints verification by integrating observers in the ε-TPN intermediate model, since TPN state-space abstractions do not allow directly such kind of model-checking.