1"use strict";(globalThis.webpackChunkcaesar_website||=[]).push([[3176],{74864(e,t,a){a.r(t),a.d(t,{default:()=>c,metadata:()=>n});var n=a(33482),s=a(74848),i=a(28453);const o={authorsImageUrls:[void 0]};function r(e){const t={a:"a",blockquote:"blockquote",em:"em",p:"p",...(0,i.R)(),...e.components};return(0,s.jsxs)(s.Fragment,{children:[(0,s.jsxs)(t.p,{children:["The paper ",(0,s.jsx)(t.a,{href:"https://doi.org/10.1007/978-3-031-75434-0_17",children:(0,s.jsx)(t.em,{children:'"A Game-Based Semantics for the Probabilistic\nIntermediate Verification Language HeyVL"'})})," by Christoph Matheja was published at ",(0,s.jsx)(t.a,{href:"https://2024-isola.isola-conference.org/",children:"AISoLA 2024"})," and is now available online."]}),"\n",(0,s.jsx)(t.p,{children:"Quoting from its abstract:"}),"\n",(0,s.jsxs)(t.blockquote,{children:["\n",(0,s.jsx)(t.p,{children:"[T]he original language [HeyVL] lacked a formal \u201cground truth\u201d in terms of a small-step operational semantics that enables an intuitive reading of HeyVL programs."}),"\n",(0,s.jsxs)(t.p,{children:["In this paper, we define an operational semantics for a cleaned-up version of HeyVL in terms of ",(0,s.jsx)(t.em,{children:"refereed"})," stochastic games, a novel extension of simple stochastic games in which a referee may perform quantitative reasoning about the expected outcome of sub-games and give one player an advantage if those sub-game are outside of certain boundaries."]}),"\n"]}),"\n",(0,s.jsx)(t.p,{children:"This new operational semantics is aimed at improved intuition and ergonomics of HeyVL, as well as a possible future work enabling other verification backends such as ones based on probabilistic model checking tools."}),"\n",(0,s.jsxs)(t.p,{children:["Note that the existing ",(0,s.jsx)(t.a,{href:"/docs/model-checking",children:"model checking backend"}),' of Caesar does not yet support for the full extent of the HeyVL language, but merely an "executable subset".\nTherefore, this publication shows an avenue for a future extension of this existing backend via refereed stochastic games.']})]})}function c(e={}){const{wrapper:t}={...(0,i.R)(),...e.components};return t?(0,s.jsx)(t,{...e,children:(0,s.jsx)(r,{...e})}):r(e)}a.d(t,["assets",0,o,"contentTitle",0,"A Game-Based Operational Semantics for HeyVL","frontMatter",0,{authors:"phisch",tags:["publications"]},"toc",0,[]])},28453(e,t,a){a.d(t,{R:()=>o,x:()=>r});var n=a(96540);const s={},i=n.createContext(s);function o(e){const t=n.useContext(i);return n.useMemo(function(){return"function"==typeof e?e(t):{...t,...e}},[t,e])}function r(e){let t;return t=e.disableParentContext?"function"==typeof e.components?e.components(s):e.components||s:o(e.components),n.createElement(i.Provider,{value:t},e.children)}},33482(e){e.exports=JSON.parse('{"permalink":"/blog/2024/12/31/game-based-semantics","editUrl":"https://github.com/moves-rwth/caesar/tree/main/website/blog/2024-12-31-game-based-semantics.md","source":"@site/blog/2024-12-31-game-based-semantics.md","title":"A Game-Based Operational Semantics for HeyVL","description":"The paper [_\\"A Game-Based Semantics for the Probabilistic","date":"2024-12-31T00:00:00.000Z","tags":[{"inline":true,"label":"publications","permalink":"/blog/tags/publications"}],"readingTime":1.03,"hasTruncateMarker":true,"authors":[{"name":"Philipp Schroer","title":"Caesar Developer","url":"https://moves.rwth-aachen.de/people/philipp-schroer/","imageURL":"https://github.com/Philipp15b.png","key":"phisch","page":null}],"frontMatter":{"authors":"phisch","tags":["publications"]},"unlisted":false,"prevItem":{"title":"Caesar 2.1: UI Improvements, More Guardrails, and Improvements to Slicing","permalink":"/blog/2025/01/17/caesar-2-1"},"nextItem":{"title":"Caesar 2.0: VSCode Extension, Slicing, and more!","permalink":"/blog/2024/05/20/caesar-2-0"}}')}}]);
Line numbers count LF bytes from the start of the resource, as the search results do. Vendor segments are library code the classifier recognised; they are stored but not indexed. Bytes are shown as Latin1 characters, one per byte.