In this work we prove decidability of the model-checking problem for safe
recursion schemes against properties defined by alternating B-automata. We then
exploit this result to show how to compute downward closures of languages of
finite trees recognized by safe recursion schemes.
Higher-order recursion schemes are an expressive formalism used to define
languages of finite and infinite ranked trees by means of fixed points of
lambda terms. They extend regular and context-free grammars, and are equivalent
in expressive power to the simply typed $\lambda Y$-calculus and collapsible
pushdown automata. Safety in a syntactic restriction which limits their
expressive power.
The class of alternating B-automata is an extension of alternating parity
automata over infinite trees; it enhances them with counting features that can
be used to describe boundedness properties.
We look in detail at the structural liveness problem (SLP) for subclasses of
Petri nets, namely immediate observation nets (IO nets) and their generalized
variant called branching immediate multi-observation nets (BIMO nets), that
were recently introduced by Esparza, Raskin, and Weil-Kennedy. We show that SLP
is PSPACE-hard for IO nets and in PSPACE for BIMO nets. In particular, we
discuss the (small) bounds on the token numbers in net places that are decisive
for a marking to be (non)live.