{"entities":{"Q7361935":{"pageid":31521344,"ns":120,"title":"Item:Q7361935","lastrevid":105370511,"modified":"2026-10-07T13:39:10Z","type":"item","id":"Q7361935","labels":{"en":{"language":"en","value":"Multi-Head Monitoring of Metric Dynamic Logic"}},"descriptions":{"en":{"language":"en","value":"AFP entry VYDRA_MDL"}},"aliases":{},"claims":{"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"fbe2fa1d579d90fdba0b555988641db811b49d7a","datavalue":{"value":"https://isa-afp.org/entries/VYDRA_MDL.html","type":"string"},"datatype":"url"},"type":"statement","id":"Q7361935$D6EC8569-6DEC-4465-B8B2-8BECCF47140D","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"4204f083ee729041d557a099dbd94c942577e22d","datavalue":{"value":{"time":"+2022-02-13T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q7361935$2C56533F-DA92-4183-BACC-D2508548E652","rank":"normal"}],"P43":[{"mainsnak":{"snaktype":"value","property":"P43","hash":"643eb3a0705e82fe3a3d92aab3f3a27de8fd83be","datavalue":{"value":"Martin Raszyk","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361935$B64D04F4-4597-49AC-950E-646C7BF62DB0","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"24bb06748e4c1a3640931aae358772a6e1bd1232","datavalue":{"value":{"text":"Multi-Head Monitoring of Metric Dynamic Logic","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q7361935$9D45754C-E17B-461C-9935-F264592609D8","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"4416fd5398cb5656a8c85f0eec557fd7c9652482","datavalue":{"value":"Runtime monitoring (or runtime verification) is an approach to checking compliance of a system's execution with a specification (e.g., a temporal formula). The system's execution is logged into a trace \u2014a sequence of time-points, each consisting of a time-stamp and observed events. A monitor is an algorithm that produces verdicts on the satisfaction of a temporal formula on a trace. We formalize the time-stamps as an abstract algebraic structure satisfying certain assumptions. Instances of this structure include natural numbers, real numbers, and lexicographic combinations of them. We also include the formalization of a conversion from the abstract time domain introduced by Koymans (1990) to our time-stamps. We formalize a monitoring algorithm for metric dynamic logic, an extension of metric temporal logic with regular expressions. The monitor computes whether a given formula is satisfied at every position in an input trace of time-stamped events. Our monitor follows the multi-head paradigm: it reads the input simultaneously at multiple positions and moves its reading heads asynchronously. This mode of operation results in unprecedented time and space complexity guarantees for metric dynamic logic: The monitor's amortized time complexity to process a time-point and the monitor's space complexity neither depends on the event-rate, i.e., the number of events within a fixed time-unit, nor on the numeric constants occurring in the quantitative temporal constraints in the given formula. The multi-head monitoring algorithm for metric dynamic logic is reported in our paper \u201cMulti-Head Monitoring of Metric Dynamic Logic\u201d published at ATVA 2020. We have also formalized unpublished specialized algorithms for the temporal operators of metric temporal logic.","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361935$A4EC4907-BDE1-4803-8BAD-5D9718070A85","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"925ab9f388dfd1680aea2355a59f16ded7291ea9","datavalue":{"value":{"entity-type":"item","numeric-id":6485872,"id":"Q6485872"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361935$D6B06038-10A2-4D54-820A-CEC40FD79E43","rank":"normal"}],"P37":[{"mainsnak":{"snaktype":"value","property":"P37","hash":"9a21a8eebe97539644aa32b24dda137c12e751dc","datavalue":{"value":{"entity-type":"item","numeric-id":40327,"id":"Q40327"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361935$A1975A11-811A-4611-9AEA-BC151D03A263","rank":"normal"}],"P585":[{"mainsnak":{"snaktype":"value","property":"P585","hash":"472350d0e5dd5ba9def2e15a38c587b54d3979fa","datavalue":{"value":{"entity-type":"item","numeric-id":7361428,"id":"Q7361428"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361935$D50CC93A-37F3-4AEA-B843-CAD738914EAA","rank":"normal"}],"P2651":[{"mainsnak":{"snaktype":"value","property":"P2651","hash":"1157f6239d5752bb0ad1cee836272bd46c6bf40f","datavalue":{"value":{"entity-type":"item","numeric-id":7360772,"id":"Q7360772"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361935$196959E3-C5E1-44F2-A4DF-BD3AA9D20A0B","rank":"normal"}],"P1460":[{"mainsnak":{"snaktype":"value","property":"P1460","hash":"908c3454b3659c4b140ccce33c5aee31081edc8d","datavalue":{"value":{"entity-type":"item","numeric-id":5976450,"id":"Q5976450"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361935$20D79825-85E5-4AD2-B133-DF3A0487D352","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Multi-Head Monitoring of Metric Dynamic Logic","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Multi-Head_Monitoring_of_Metric_Dynamic_Logic"}}}}}