Zobrazeno 1 - 10
of 217
pro vyhledávání: '"PERON, ADRIANO"'
Characterisations theorems serve as important tools in model theory and can be used to assess and compare the expressive power of temporal languages used for the specification and verification of properties in formal methods. While complete connectio
Externí odkaz:
http://arxiv.org/abs/2404.17421
Monadic Second-Order Logic (MSO) extends First-Order Logic (FO) with variables ranging over sets and quantifications over those variables. We introduce and study Monadic Tree Logic (MTL), a fragment of MSO interpreted on infinite-tree models, where t
Externí odkaz:
http://arxiv.org/abs/2304.11613
Autor:
Bozzelli, Laura, Peron, Adriano
Publikováno v:
EPTCS 370, 2022, pp. 97-113
Model checking for Halpern and Shoham's interval temporal logic HS has been recently investigated in a systematic way, and it is known to be decidable under three distinct semantics. Here, we focus on the trace-based semantics, where the infinite exe
Externí odkaz:
http://arxiv.org/abs/2209.10316
Hyperproperties are properties of systems that relate different executions traces, with many applications from security to symmetry, consistency models of concurrency, etc. In recent years, different linear-time logics for specifying asynchronous hyp
Externí odkaz:
http://arxiv.org/abs/2207.02956
Autor:
Bozzelli, Laura, Peron, Adriano
Model checking for Halpern and Shoham's interval temporal logic HS has been recently investigated in a systematic way, and it is known to be decidable under three distinct semantics (state-based, trace-based and tree-based semantics). Here, we focus
Externí odkaz:
http://arxiv.org/abs/2206.13920
Publikováno v:
EPTCS 346, 2021, pp. 179-194
The choice of the right trade-off between expressiveness and complexity is the main issue in interval temporal logic. In their seminal paper, Halpern and Shoham showed that the satisfiability problem for HS (the temporal logic of Allen's relations) i
Externí odkaz:
http://arxiv.org/abs/2109.08320
In the context of End-to-End testing of web applications, automated exploration techniques (a.k.a. crawling) are widely used to infer state-based models of the site under test. These models, in which states represent features of the web application a
Externí odkaz:
http://arxiv.org/abs/2108.13322
Publikováno v:
LICS 2021
Hyperproperties are a modern specification paradigm that extends trace properties to express properties of sets of traces. Temporal logics for hyperproperties studied in the literature, including HyperLTL, assume a synchronous semantics and enjoy a d
Externí odkaz:
http://arxiv.org/abs/2104.12886
Publikováno v:
Logical Methods in Computer Science, Volume 18, Issue 1 (February 1, 2022) lmcs:6542
The expressive power of interval temporal logics (ITLs) makes them one of the most natural choices in a number of application domains, ranging from the specification and verification of complex reactive systems to automated planning. However, for a l
Externí odkaz:
http://arxiv.org/abs/2006.04652
In this paper, we investigate the module-checking problem of pushdown multi-agent systems (PMS) against ATL and ATL* specifications. We establish that for ATL, module checking of PMS is 2EXPTIME-complete, which is the same complexity as pushdown modu
Externí odkaz:
http://arxiv.org/abs/2003.04728