arXiv subjects

Wang Yi

Publications and source records attributed to Wang Yi.

21 records · Page 2Linked to original sources

arXiv2015

Time-resolved measure technique for electron beam envelope basing on synchronous framing and streaking principle

The time-resolved electron beam envelope parameters including sectional distribution and position are important and necessary for the study of beam transmission characteristics in the magnetic field and verifying the magnetic field setup rationality. One kind of high time-resolved beam envelope measurement system has developed recently. It is mainly constituted of high framing camera and streak camera. It can obtain 3 panoramic images of the beam and the time continuous information of the given beam cross section at one time. The recently obtained data has proved that several fast vibration of beam envelope along the diameter direction occur during the rising edge and the falling edge of the electron beam. The vibration period is about several nanoseconds. The effect of magnetic field on the electron beam is also observed and verified. The beam debug experiments have proved that the existing beam transmission design is reasonable and viable. The beam envelope measurement system will establish a good foundation for beam physics research.

physics.acc-ph↗

arXiv2014

Horn Clauses for Communicating Timed Systems

Languages based on the theory of timed automata are a well established approach for modelling and analysing real-time systems, with many applications both in industrial and academic context. Model checking for timed automata has been studied extensively during the last two decades; however, even now industrial-grade model checkers are available only for few timed automata dialects (in particular Uppaal timed automata), exhibit limited scalability for systems with large discrete state space, or cannot handle parametrised systems. We explore the use of Horn constraints and off-the-shelf model checkers for analysis of networks of timed automata. The resulting analysis method is fully symbolic and applicable to systems with large or infinite discrete state space, and can be extended to include various language features, for instance Uppaal-style communication/broadcast channels and BIP-style interactions, and systems with infinite parallelism. Experiments demonstrate the feasibility of the method.

cs.LO↗

arXiv2010

Sampled Semantics of Timed Automata

Sampled semantics of timed automata is a finite approximation of their dense time behavior. While the former is closer to the actual software or hardware systems with a fixed granularity of time, the abstract character of the latter makes it appealing for system modeling and verification. We study one aspect of the relation between these two semantics, namely checking whether the system exhibits some qualitative (untimed) behaviors in the dense time which cannot be reproduced by any implementation with a fixed sampling rate. More formally, the \emph{sampling problem} is to decide whether there is a sampling rate such that all qualitative behaviors (the untimed language) accepted by a given timed automaton in dense time semantics can be also accepted in sampled semantics. We show that this problem is decidable.

cs.FL↗