Linux has its own kernel, written originally by Linus Torvalds. Android, GNU, and others run on top of it...I have to assume that you're about either st.com or stmicroelectronics.com.cn. They have documentation on OS20. It clearly states that OS20 is a real time kernel and as such, there must be an actual OS running on top of it (i.e. DOS, Linux, Unix, Windows, etc.). Since the filesystem is of the EXTn family, the logical assumption is that Linux is that operating system.
The Echostar Knowledge Database (EKB) and other sources are clear about the PVR501 using OpenTV 2.0 but they don't cite the underlying OS.