A Counting Logic for Structure Transition Systems

摘要

Quantitative questions such as "what is the maximum number of tokens in a place of a Petri net?" or "what is the maximal reachable height of the stack of a pushdown automaton?" play a significant role in understanding models of computation. To study such