Pete Austin, Sougata Bose, Nicolas Mazzocchi and Patrick Totzke.
Temporal Explorability Games
Frédéric Herbreteau, Sarah Larroze and Igor Walukiewicz.
Partial-Order Reduction Is Hard
Yangluo Zheng.
Reachability in Vector Addition System with States Parameterized by Geometric Dimension
Noam Zilberstein, Daniele Gorla and Alexandra Silva.
Denotational Semantics for Probabilistic and Concurrent Programs
Nicolaj Østerby Jensen, Kim Guldstrand Larsen, Didier Lime and Jiri Srba.
On-The-Fly Symbolic Algorithm for Timed ATL1 with Abstractions
Sarah Winter and Martin Zimmermann.
Prophecies all the Way: Game-based Model-Checking for HyperQPTL beyond ∀*∃*
Caroline Lemke and Benjamin Bisping.
Galois Energy Games: To Solve All Kinds of Quantitative Reachability Problems
Luca Aceto, Antonis Achilleos, Ducan Paul Attard, Léo Exibard, Adrian Francalanza, Anna Ingolfsdottir and Karoliina Lehtinen.
Monitorability for the Modal µ-Calculus over Systems with Data: From Practice to Theory
Laura Bocchi, Andy King, Maurizio Murgia and Simon Thompson.
Abstract Subtyping for Asynchronous Multiparty Sessions
Yun Chen Tsai, Kittiphon Phalakarn, S. Akshay and Ichiro Hasuo.
Chance and Mass Interpretations of Probabilities in Markov Decision Processes
Rowin Versteeg, Valentina Castiglioni and Bas Luttik.
From Bisimulation to Traces: The Impact of Parallel Composition on Finite Bases
Francois Laroussinie and Nicolas Markey.
Arbitrary-arity Tree Automata for QCTL
Wojciech Czerwiński and Łukasz Orlikowski.
Languages of Boundedly-Ambiguous Vector Addition Systems with States
Paolo Baldan, Roberto Bruni, Francesco Ranzato and Diletta Rigo.
Model Checking as Program Verification by Abstract Interpretation
Daniel Hirschkoff, Iwan Quémerais and Davide Sangiorgi.
First-order store and visibility in name-passing calculi
Jan Friso Groote and David N. Jansen.
A state-based O(m log n) partitioning algorithm for branchingbisimilarity
Raphaël Berthon, Joost-Pieter Katoen and Zihan Zhou.
A Direct Reduction from Parity to Simple Stochastic Games
Thomas Henzinger, Pavol Kebis, Nicolas Mazzocchi and N. Ege Saraç.
Quantitative Language Automata
Soumyajit Paul, David Purser, Sven Schewe, Qiyi Tang, Patrick Totzke and Di-De Yen.
Resolving Nondeterminism by Chance
Bharat Adsul, Paul Gastin and Shantanu Kulkarni.
Characterizations of fragments of temporal logic over Mazurkiewikz traces
Frits Vaandrager and Ivo Melse.
New Fault Domains for Conformance Testing of Finite State Machines
Rob van Glabbeek, Bas Luttik and Myrthe Spronck.
Just Verification of Mutual Exclusion Algorithms
Hannah Mertens, Tim Quatmann and Joost-Pieter Katoen.
Compositional Reasoning for Parametric Probabilistic Automata
Luc Dartois, Paul Gastin, Loic Germerie Guizouarn and S Krishna.
Reversible Pebble Transducers
Emily Vlasman, James Worrell, Anto Nanah Ji and Franck van Breugel.
Explainability is a Game for Probabilistic Bisimilarity Distances
Noam Shenwald and Orna Kupferman.
Coverage Games
Tiange Liu, Alwen Tiu and Ross Horne.
Open Bisimilarity for the π-calculus with Mismatch
Thomas Møller Grosen, Sean Kauffman, Kim G. Larsen and Martin Zimmermann.
Time for Timed Monitorability
S. Akshay, Ouldouz Neysari and Đorđe Žikelić.
Omega-regular Verification and Control for Distributional Specifications in MDPs
Laurent Doyen, Pranshu Gaba and Shibashis Guha.
Expectation in Stochastic Games with Prefix-independent Objectives
Hsi-Ming Ho, S Krishna, Khushraj Madnani, Rupak Majumdar and Paritosh Pandya.
Expressive Equivalence Between Decidable Freeze and Metric Timed Temporal Logics
Mario Bravetti, Luca Padovani and Gianluigi Zavattaro.
A Sound and Complete Characterization of Fair Asynchronous Session Subtyping
Véronique Bruyère, Jean-Francois Raskin, Alexis Reynouard and Marie Van Den Bogaard.
The Non-Cooperative Rational Synthesis Problem for Subgame Perfect Equilibria and omega-regular Objectives
Mohammad Hossein Khoshechin Jorshari, Michalis Kokologiannakis, Rupak Majumdar and Srinidhi Nagendra.
Optimal Concolic Dynamic Partial Order Reduction
Leo Henry, Thomas Neele, Mohammad Mousavi and Matteo Sammartino.
Compositional Active Learning of Synchronous Systems through Automated Alphabet Refinement
Romain Delpy, Anca Muscholl and Grégoire Sutre.
On the send-synchronizability problem for mailbox communication