the proceedings contain 19 papers. the special focus in this conference is on foundations of softwarescience and computationstructures. the topics include: Fair Quantitative Games;model-Checking Real-Time Systems: R...
ISBN:
(纸本)9783031908965
the proceedings contain 19 papers. the special focus in this conference is on foundations of softwarescience and computationstructures. the topics include: Fair Quantitative Games;model-Checking Real-Time Systems: Revisiting the Alternating Automaton Route;two-sorted algebraic decompositions of Brookes’s shared-state denotational semantics;idempotent Resources in Separation Logic: the Heart of core in Iris;a Behavioural Pseudometric for Continuous-Time Markov Processes;complementation of Emerson-Lei Automata;alternative Characterizations of Hereditary History-Preserving Bisimilarity via Backward Ready Multisets;context-Free Languages of String Diagrams;relational Connectors and Heterogeneous Simulations;on the cut-elimination of the modal μ-calculus: Linear Logic to the rescue;combining quantum and classical control: syntax, semantics and adequacy;BiGKAT: An Algebraic Framework for Relational Verification of Probabilistic Programs;sharing and Linear Logic with Restricted Access;a General Completeness theorem for Skip-Free Star Algebras;complete Test Suites for Automata in Monoidal Closed Categories;temporal Hyperproperties for Population Protocols;preface;ETAPS Foreword.
the proceedings contain 12 papers. the special focus in this conference is on foundations of softwarescience and computationstructures. the topics include: From Rewrite Rules to Axioms in the λΠ-Calculus Modulo th...
ISBN:
(纸本)9783031572302
the proceedings contain 12 papers. the special focus in this conference is on foundations of softwarescience and computationstructures. the topics include: From Rewrite Rules to Axioms in the λΠ-Calculus Modulo theory;light Genericity;logical Predicates in Higher-Order Mathematical Operational Semantics;on Basic Feasible Functionals and the Interpretation Method;Succinctness of Cosafety Fragments of LTL via Combinatorial Proof Systems;A Resolution-Based Interactive Proof System for UNSAT;craig Interpolation for Decidable First-Order Fragments;clones, closed categories, and combinatory logic;Reachability in Fixed VASS: Expressiveness and Lower Bounds;from Innermost to Full Almost-Sure Termination of Probabilistic Term Rewriting;dimension-Minimality and Primality of Counter Nets.
the proceedings contain 12 papers. the special focus in this conference is on foundations of softwarescience and computationstructures. the topics include: From Rewrite Rules to Axioms in the λΠ-Calculus Modulo th...
ISBN:
(纸本)9783031572272
the proceedings contain 12 papers. the special focus in this conference is on foundations of softwarescience and computationstructures. the topics include: From Rewrite Rules to Axioms in the λΠ-Calculus Modulo theory;light Genericity;logical Predicates in Higher-Order Mathematical Operational Semantics;on Basic Feasible Functionals and the Interpretation Method;Succinctness of Cosafety Fragments of LTL via Combinatorial Proof Systems;A Resolution-Based Interactive Proof System for UNSAT;craig Interpolation for Decidable First-Order Fragments;clones, closed categories, and combinatory logic;Reachability in Fixed VASS: Expressiveness and Lower Bounds;from Innermost to Full Almost-Sure Termination of Probabilistic Term Rewriting;dimension-Minimality and Primality of Counter Nets.
the proceedings contain 23 papers. the special focus in this conference is on foundations of softwarescience and computationstructures. the topics include: A new criterion for M, N -adhesivity, with an application t...
ISBN:
(纸本)9783030992521
the proceedings contain 23 papers. the special focus in this conference is on foundations of softwarescience and computationstructures. the topics include: A new criterion for M, N -adhesivity, with an application to hierarchical graphs;quantifier elimination for counting extensions of Presburger arithmetic;a first-order logic characterisation of safety and co-safety languages;first-order separation over countable ordinals;a Faithful and Quantitative Notion of Distant Reduction for Generalized Applications;modal Logics and Local Quantifiers: A Zoo in the Elementary Hierarchy;temporal Stream Logic modulo theories;the Different Shades of Infinite Session Types;complete and tractable machine-independent characterizations of second-order polytime;limits and difficulties in the design of under-approximation abstract domains;variable binding and substitution for (nameless) dummies;uniform Guarded Fragments;sweedler theory of Monads;model Checking Temporal Properties of Recursive Probabilistic Programs;on probability-raising causality in Markov decision processes;parameterized Analysis of Reconfigurable Broadcast Networks;separators in Continuous Petri Nets;graphical Piecewise-Linear Algebra;token Games and History-Deterministic Quantitative Automata;on the Translation of Automata to Linear Temporal Logic.
the proceedings contain 28 papers. the special focus in this conference is on foundations of softwarescience and computationstructures. the topics include: Finding cut-offs in leaderless rendez-vous protocols is eas...
ISBN:
(纸本)9783030719944
the proceedings contain 28 papers. the special focus in this conference is on foundations of softwarescience and computationstructures. the topics include: Finding cut-offs in leaderless rendez-vous protocols is easy;fixpoint theory – upside down;"Most of" leads to undecidability: Failure of adding frequencies to LTL;combining semilattices and semimodules;one-way resynchronizability of word transducers;fair refinement for asynchronous session types;running time analysis of broadcast consensus protocols;leafy automata for higher-order concurrency;factorization in call-by-name and call-by-value calculi via linear logic;generalized bounded linear logic and its categorical semantics;focused proof-search in the logic of bunched implications;interpolation and amalgamation for arrays with maxdiff;adjoint reactive gui programming;on the expressiveness of büchi arithmetic;learning pomset automata;parametricity for primitive nested types;the spirit of node replication;nondeterministic and co-nondeterministic implies deterministic, for data languages;certifying inexpressibility;a general semantic construction of dependent refinement type systems, categorically;simple stochastic games with almost-sure energy-parity objectives are in np and conp;nondeterministic syntactic complexity;a string diagrammatic axiomatisation of finite-state automata;work-sensitive dynamic complexity of formal languages;the structure of sum-over-paths, its consequences, and completeness for clifford;a quantified coalgebraic van benthem theorem.
there are many evaluation strategies for term rewrite systems, but proving termination automatically is usually easiest for innermost rewriting. Several syntactic criteria exist when innermost termination implies full...
详细信息
ISBN:
(纸本)9783031572302;9783031572319
there are many evaluation strategies for term rewrite systems, but proving termination automatically is usually easiest for innermost rewriting. Several syntactic criteria exist when innermost termination implies full termination. We adapt these criteria to the probabilistic setting, e.g., we show when it suffices to analyze almost-sure termination (AST) w.r.t. innermost rewriting to prove full AST of probabilistic term rewrite systems. these criteria also apply to other notions of termination like positive AST. We implemented and evaluated our new contributions in the tool AProVE.
this paper focuses on succinctness results for fragments of Linear Temporal Logic with Past (LTL) devoid of binary temporal operators like until, and provides methods to establish them. We prove that there is a family...
详细信息
ISBN:
(纸本)9783031572302;9783031572319
this paper focuses on succinctness results for fragments of Linear Temporal Logic with Past (LTL) devoid of binary temporal operators like until, and provides methods to establish them. We prove that there is a family of cosafety languages (L-n) n >= 1 such that Ln can be expressed with a pure future formula of size O(n), but it requires formulae of size 2(Omega(n)) to be captured with past formulae. As a by-product, such a succinctness result shows the optimality of the pastification algorithm proposed in [Artale et al., KR, 2023]. We show that, in the considered case, succinctness cannot be proven by relying on the classical automata-based method introduced in [Markey, Bull. EATCS, 2003]. In place of this method, we devise and apply a combinatorial proof system whose deduction trees represent LTL formulae. the system can be seen as a proof-centric (one-player) view on the games used by Adler and Immerman to study the succinctness of CTL.
We consider two-player games over finite graphs in which both players are restricted by fairness constraints on their moves. Given a two player game graph G = (V, E) and a set of fair moves E-f subset of E a player is...
详细信息
ISBN:
(纸本)9783031572272;9783031572289
We consider two-player games over finite graphs in which both players are restricted by fairness constraints on their moves. Given a two player game graph G = (V, E) and a set of fair moves E-f subset of E a player is said to play fair in G if they choose an edge e is an element of E-f infinitely often whenever the source node of e is visited infinitely often. Otherwise, they play unfair. We equip such games with two w -regular winning conditions alpha and beta deciding the winner of mutually fair and mutually unfair plays, respectively. Whenever one player plays fair and the other plays unfair, the fairly playing player wins the game. the resulting games are called fair alpha/beta games. We formalize fair alpha/beta games and show that they are determined. For fair parity/parity games, i.e., fair alpha/beta games where alpha and beta are given each by a parity condition over G, we provide a polynomial reduction to (normal) parity games via a gadget construction inspired by the reduction of stochastic parity games to parity games. We further give a direct symbolic fixpoint algorithm to solve fair parity/parity games. On a conceptual level, we illustrate the translation between the gadget -based reduction and the direct symbolic algorithm which uncovers the underlying similarities of solution algorithms for fair and stochastic parity games, as well as for the recently considered class of fair games in which only one player is restricted by fair moves.
We introduce context-free languages of morphisms in monoidal categories, extending recent work on the categorification of context-free languages, and regular languages of string diagrams. Context-free languages of str...
详细信息
We show that the EXPSPACE-hardness result for structural liveness of Petri nets [Jančar and Purser, 2019] holds even for a60;simple subclass of conservative nets. As the main result we then show that for structural...
详细信息
暂无评论