{"entities":{"Q7361382":{"pageid":31519685,"ns":120,"title":"Item:Q7361382","lastrevid":105365279,"modified":"2026-10-07T13:35:46Z","type":"item","id":"Q7361382","labels":{"en":{"language":"en","value":"Transition Systems and Automata"}},"descriptions":{"en":{"language":"en","value":"AFP entry Transition_Systems_and_Automata"}},"aliases":{},"claims":{"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"3e5ebb052c1f1d23cd7d112004e41fecc2906555","datavalue":{"value":"https://isa-afp.org/entries/Transition_Systems_and_Automata.html","type":"string"},"datatype":"url"},"type":"statement","id":"Q7361382$4828E846-1758-483D-85FC-E6F6674831DB","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"09fed704422914cfe2a4482b61f3f610c89a1884","datavalue":{"value":{"time":"+2017-10-19T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q7361382$4F87F674-AC4D-4FCD-B40B-FE0F560D19AE","rank":"normal"}],"P43":[{"mainsnak":{"snaktype":"value","property":"P43","hash":"858e1b98f2a2702d86b0690e1e15aa540fc68e16","datavalue":{"value":"Julian Brunner","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361382$0E99D06D-F895-4A2E-A2E3-705DAAA1AD47","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"d01f295bc1c9d9262ae012884897529fa3074807","datavalue":{"value":{"text":"Transition Systems and Automata","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q7361382$6CA38C05-166A-4C56-8AFD-97E254281834","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"e69ae0a2b1cf7a47f9e8badf883496bca84f6dd7","datavalue":{"value":"This entry provides a very abstract theory of transition systems that can be instantiated to express various types of automata. A transition system is typically instantiated by providing a set of initial states, a predicate for enabled transitions, and a transition execution function. From this, it defines the concepts of finite and infinite paths as well as the set of reachable states, among other things. Many useful theorems, from basic path manipulation rules to coinduction and run construction rules, are proven in this abstract transition system context. The library comes with instantiations for DFAs, NFAs, and B\u00fcchi automata.","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361382$2E4D4BC7-FBB1-47A7-B0F7-E413761995F1","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":"Q7361382$798FD542-BCF9-490A-B3E4-A2830B93F4B8","rank":"normal"}],"P585":[{"mainsnak":{"snaktype":"value","property":"P585","hash":"f0d6ccc9a00d2d1e3be7ec2239689671c14dec25","datavalue":{"value":{"entity-type":"item","numeric-id":7361918,"id":"Q7361918"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361382$C8A45456-72C8-4E31-B98A-FBEE0FFED9D6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P585","hash":"c0e4b154d3cbaa6adcd084b741855073f781fcfd","datavalue":{"value":{"entity-type":"item","numeric-id":7361011,"id":"Q7361011"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361382$8A1DC432-239E-4A6F-B720-E6F5C4CC8514","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P585","hash":"fd79867ce10ec25799473c4691ec619caa547136","datavalue":{"value":{"entity-type":"item","numeric-id":7361723,"id":"Q7361723"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361382$78198829-67AF-409B-BD54-F5800BED1410","rank":"normal"}],"P2651":[{"mainsnak":{"snaktype":"value","property":"P2651","hash":"73d93a21b0749f7f2c51d7daeb11b162660cd756","datavalue":{"value":{"entity-type":"item","numeric-id":7360784,"id":"Q7360784"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361382$EA52E4D3-EA13-4982-BA80-F09539352586","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":"Q7361382$39365A1D-DF32-45B5-A3FE-A7135A1A36CC","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Transition Systems and Automata (AFP entry Transition Systems and Automata)","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Transition_Systems_and_Automata_(AFP_entry_Transition_Systems_and_Automata)"}}}}}