相关论文: Indefinite waitings in MIRELA systems

Identifying a temporal pattern of events is a fundamental task of on-line (real-time) verification. We present efficient schemes for on-line monitoring of events for identifying desired/undesired patterns of events. The schemes use…

Operating LLMs as coordinated multi-agent research systems over multi-hour runs surfaces failure modes that single-shot evaluation cannot: upstream providers throttle without warning, sub-agents drift the task to fit accessible tools,…

From biological systems to cyber-physical systems, monitoring the behavior of such dynamical systems often requires to reason about complex spatio-temporal properties of physical and/or computational entities that are dynamically…

Modern intelligent systems researchers form hypotheses about system behavior and then run experiments using one or more independent variables to test their hypotheses. We present SIERRA, a novel framework structured around that idea for…

Model checking properties are often described by means of finite automata. Any particular such automaton divides the set of infinite trees into finitely many classes, according to which state has an infinite run. Building the full type…

This paper is a survey of extensions to finite automata theory to model real-time systems as well as systems exhibiting mixed discrete-continuous behavior. Real-time systems maintain a continuous and timely interaction with the environment,…

One clock alternating timed automata (OCATA) have been introduced as natural extension of (one clock) timed automata to express the semantics of MTL. In this paper, we consider the application of OCATA to the problems of model-checking and…

This work is devoted to the study of the capabilities of the Modelica and Julia programming languages for the implementation of a continuously discrete paradigm in modeling hybrid systems that contain both continuous and discrete aspects of…

This paper describes a static verification framework for the message-passing fragment of the Go programming language. Our framework extracts models that over-approximate the message-passing behaviour of a program. These models, or…

Railway scheduling consists in ensuring that a set of trains evolve in a shared rail network without collisions, while meeting schedule constraints. This problem is notoriously difficult, even more in the case of uncertain or even unknown…

This paper is about modeling and verification languages with their pros and cons. Modeling is dynamic part of system development process before realization. The cost and risky situations obligate designer to model system before production…

Model checking is a powerful method widely explored in formal verification. Given a model of a system, e.g., a Kripke structure, and a formula specifying its expected behaviour, one can verify whether the system meets the behaviour by…

Metric Interval Temporal Logic (MITL) is a popular formalism for specifying properties of reactive systems with timing constraints. Existing approaches to using MITL in verification tasks, however, have notable drawbacks: they either…

This paper proposes the use of model-checking software technology for the verification of workflows and business processes behaviour based on web services, namely the use of the SPIN model checker. Since the specification of a business…

Time-invariant finite-dimensional systems, under reasonable continuity assumptions, exhibit the property that if solutions exist for all future times, the set of vectors reachable from a bounded set of initial conditions over bounded time…

MITL is a temporal logic that facilitates the verification of real-time systems by expressing the critical timing constraints placed on these systems. MITL specifications can be checked against system models expressed as networks of timed…

A feature of current membrane systems is the fact that objects and membranes are persistent. However, this is not true in the real world. In fact, cells and intracellular proteins have a well-defined lifetime. Inspired from these biological…

Hybrid systems are dynamical systems with continuous evolution of states and discrete evolution of states and governing equations. We have worked on the design and implementation of HydLa, a constraint-based modeling language for hybrid…

Modern intelligent systems researchers employ the scientific method: they form hypotheses about system behavior, and then run experiments using one or more independent variables to test their hypotheses. We present SIERRA, a novel framework…

CoInDiVinE is a tool for parallel distributed model checking of interactions among components in hierarchical component-based systems. The tool extends the DiVinE framework with a new input language (component-interaction automata) and a…