neutralize
发表于 2025-3-23 11:15:33
MetateM: A framework for programming in temporal logic,ab87, Gab89] and present a concrete framework, called . for executing (modal and) temporal logics. Our approach is illustrated by the development of an execution mechanism for a propositional temporal logic and for a restricted first order temporal logic.
gastritis
发表于 2025-3-23 17:21:46
http://reply.papertrans.cn/88/8774/877334/877334_12.png
groggy
发表于 2025-3-23 20:35:56
http://reply.papertrans.cn/88/8774/877334/877334_13.png
Blasphemy
发表于 2025-3-23 23:30:31
http://reply.papertrans.cn/88/8774/877334/877334_14.png
COWER
发表于 2025-3-24 04:54:33
Abadi & Lamport and stark: Towards a proof theory for stuttering, dense domains and refinement mappn the other hand they introduce stuttering and, in the case of refinement mappings, lead to the non-existence of such mappings..Semantically, the these problems are solved satisfactorily in the work of Abadi & Lamport . Syntactically, however, their solutions have no obvious prooftheoretic cou
kidney
发表于 2025-3-24 09:18:52
http://reply.papertrans.cn/88/8774/877334/877334_16.png
秘密会议
发表于 2025-3-24 11:31:52
Refinement of actions in causality based models, by more complicated processes on a lower level. This is done in such a way that the behaviour of the refined system may be inferred compositionally from the behaviour of the original system and from the behaviour of the processes substituted for actions. We define this refinement operation for caus
Control-Group
发表于 2025-3-24 17:38:04
Transformation of combined data type and process specifications using projection algebras,mework of metric spaces. It allows to combine data type- and process specifications within one formalism. Parameterized projection specifications, corresponding to usual algebraic parameterized specifications, carry over compositionality to combined data type and process specifications. The paramete
PHAG
发表于 2025-3-24 21:59:13
Various simulations and refinements,ition system. The concept of simulation is presented and proved to be sound for correctness of implementation. The paper provides a rigorous method for the formal development of communicating processes by integrating the event-based approach (such as CSP and CCS ) with the state-based techniq
矛盾心理
发表于 2025-3-25 02:02:10
On decomposing and refining specifications of distributed systems, system is specified through the sequence of messages that can be sent and received in an execution of the system. We use . to specify such sequences in analogy with the way finite automata are used as acceptors of finite strings. Safety properties are specified by the set of transitions of the tran