Branching-time type operators on finite pseudo-Boolean algebras

Branching-time type operators on pseudo-Boolean algebras (PBAs) are considered. It is proved that on a finite PBA, every operator of this type is defined by a subset of points on a finite frame presenting that PBA.