Hi RTAMT maintainers,
URML (urml.dev) is a small, Apache-2.0 language for describing robot intent. It validates a request statically against a capability manifest and a safety envelope, then dispatches. The envelope is the part this issue is about: today it is a set of declared limits (geofence, occupancy, velocity and altitude bounds, link-loss rules) that URML checks before anything moves. What it is not yet is a set of monitorable temporal-logic properties, and RTAMT is the obvious vocabulary for that.
Nothing here asks RTAMT to change or maintain anything. This is a request for comment on a clean division of labor.
URML is static and pre-dispatch: it rejects an inadmissible request before execution. A runtime monitor is the complement: it catches a violation of an envelope property during execution. So two real questions. First, is it sound to express a URML safety-envelope property (a geofence held over time, a velocity bound) as an STL formula that RTAMT monitors, and are there envelope shapes that resist a clean STL encoding? Second, what signal interface does an online RTAMT monitor expect, so URML could emit the right traces from a running program?
Full write-up, with the envelope-to-STL mapping: https://github.com/URML-MARS/URML/blob/main/docs/rfcs/0362-rtamt-outreach.md
Thanks for RTAMT; an approachable open STL monitor is exactly the missing piece for a lot of us.
Ido Yahalomi (URML, greenvh@gmail.com)
AI-assisted prose, maintainer-reviewed before posting (see VIBE.md). Human-only correspondence available on request.
Hi RTAMT maintainers,
URML (urml.dev) is a small, Apache-2.0 language for describing robot intent. It validates a request statically against a capability manifest and a safety envelope, then dispatches. The envelope is the part this issue is about: today it is a set of declared limits (geofence, occupancy, velocity and altitude bounds, link-loss rules) that URML checks before anything moves. What it is not yet is a set of monitorable temporal-logic properties, and RTAMT is the obvious vocabulary for that.
Nothing here asks RTAMT to change or maintain anything. This is a request for comment on a clean division of labor.
URML is static and pre-dispatch: it rejects an inadmissible request before execution. A runtime monitor is the complement: it catches a violation of an envelope property during execution. So two real questions. First, is it sound to express a URML safety-envelope property (a geofence held over time, a velocity bound) as an STL formula that RTAMT monitors, and are there envelope shapes that resist a clean STL encoding? Second, what signal interface does an online RTAMT monitor expect, so URML could emit the right traces from a running program?
Full write-up, with the envelope-to-STL mapping: https://github.com/URML-MARS/URML/blob/main/docs/rfcs/0362-rtamt-outreach.md
Thanks for RTAMT; an approachable open STL monitor is exactly the missing piece for a lot of us.
Ido Yahalomi (URML, greenvh@gmail.com)
AI-assisted prose, maintainer-reviewed before posting (see VIBE.md). Human-only correspondence available on request.