Verification of two-variable logic revisited

Verification of two-variable logic revisited

Two-variable logic (FO2) is a fragment of first-order logic that allows for decidable verification problems. In previous work [2], we developed an approach to FO2 verification that is particularly useful for probabilistic systems, based on analysis of the translation of FO2 to automata. In this work...

Volledige beschrijving

Bibliografische gegevens
Hoofdauteurs:	Benedikt, M, Lenhardt, R, Worrell, J
Formaat:	Journal article
Taal:	English
Gepubliceerd in:	2012

Gelijkaardige items

TWO VARIABLE VS. LINEAR TEMPORAL LOGIC IN MODEL CHECKING AND GAMES
door: Benedikt, M, et al.
Gepubliceerd in: (2013)

Two Variable vs. Linear Temporal Logic in Model Checking and Games
door: Benedikt, M, et al.
Gepubliceerd in: (2011)

Complexity of two-variable logic on finite trees
door: Benaim, S, et al.
Gepubliceerd in: (2016)

Two variable and linear temporal logic in model checking and games
door: Lenhardt, R
Gepubliceerd in: (2013)

Two variable logic with ultimately periodic counting
door: Benedikt, M, et al.
Gepubliceerd in: (2020)

Two variable logic with ultimately periodic counting
door: Benedikt, M, et al.
Gepubliceerd in: (2024)

LTL model checking of interval Markov chains
door: Benedikt, M, et al.
Gepubliceerd in: (2013)

Logic synthesis and verification algorithms /
door: 427444 Hachtel, Gary D., et al.
Gepubliceerd in: (2006)

Higher Order Logic and Hardware Verification
door: Melham, T
Gepubliceerd in: (1993)

Time-Bounded Verification
door: Ouaknine, J, et al.
Gepubliceerd in: (2009)

Hardware Verification using Higher−Order Logic
door: Camilleri, A, et al.
Gepubliceerd in: (1986)

Hardware Verification using Higher−Order Logic
door: Camilleri, A, et al.
Gepubliceerd in: (1987)

Revisiting the Equivalence Problem for Finite Multitape Automata
door: Worrell, J
Gepubliceerd in: (2013)

Revisiting reachability in timed automata
door: Quaas, K, et al.
Gepubliceerd in: (2017)

The Expressive Power of Two−Variable Least Fixed−Point Logics
door: Grohe, M, et al.
Gepubliceerd in: (2005)

Responsibility and verification: importance value in temporal logics
door: Mascle, C, et al.
Gepubliceerd in: (2021)

Towards a Theory of Time-Bounded Verification.
door: Ouaknine, J, et al.
Gepubliceerd in: (2010)

On automated verification of probabilistic programs
door: Legay, A, et al.
Gepubliceerd in: (2008)

Two hits revisited again.
door: Tomlinson, I, et al.
Gepubliceerd in: (2001)

Using Propositional Logic for Requirements Verification of Service Workflow
door: Xu, L, et al.
Gepubliceerd in: (2012)

Using Propositional Logic for Requirements Verification of Service Workflow
door: Xu, L, et al.
Gepubliceerd in: (2012)

Variable Precision Logic
door: Michalski, Ryszard S., et al.
Gepubliceerd in: (2004)

Variables as Resource in Separation Logic
door: Bornat, R, et al.
Gepubliceerd in: (2006)

Formal verification and dynamic validation of logic-based control systems
door: Park, Taeshin, 1966-
Gepubliceerd in: (2010)

Formalizing Abstraction Mechanisms for Hardware Verification in Higher Order Logic
door: Melham, T
Gepubliceerd in: (1989)

Norman Angell and the logic of economic interdependence revisited: 1914, 2014
door: Tan, Er-Win, et al.
Gepubliceerd in: (2015)

Access Patterns and Integrity Constraints Revisited
door: Barany, V, et al.
Gepubliceerd in: (2013)

On the decidability of Metric Temporal Logic
door: Ouaknine, J, et al.
Gepubliceerd in: (2005)

Safety metric temporal logic is fully decidable
door: Ouaknine, J, et al.
Gepubliceerd in: (2006)

On metric temporal logic and faulty turing machines
door: Ouaknine, J, et al.
Gepubliceerd in: (2006)

Some Recent Results in Metric Temporal Logic
door: Ouaknine, J, et al.
Gepubliceerd in: (2008)

Interaction revisited: the difference between two estimates.
door: Altman, D, et al.
Gepubliceerd in: (2003)

Interaction revisited: the difference between two estimates.
door: Altman, D, et al.
Gepubliceerd in: (2003)

Online Monitoring of Metric Temporal Logic
door: Ho, H, et al.
Gepubliceerd in: (2014)

Modeling, simulation and experimental verification of variable parameter of suspension spring
door: Wan Ahmad Syafiq, Wan Ghafar
Gepubliceerd in: (2013)

Testing semantics: Connecting processes and process logics
door: Pavlovic, D, et al.
Gepubliceerd in: (2006)

Testing semantics: Connecting processes and process logics
door: Pavlovic, D, et al.
Gepubliceerd in: (2006)

From XQuery to Relational Logics
door: Benedikt, M, et al.
Gepubliceerd in: (2009)

On Process−algebraic Extensions of Metric Temporal Logic
door: Haase, C, et al.
Gepubliceerd in: (2010)

ON THE DECIDABILITY AND COMPLEXITY OF METRIC TEMPORAL LOGIC OVER FINITE WORDS
door: Ouaknine, J, et al.
Gepubliceerd in: (2007)