Abstract: Temporal logics are extensively used to reason about correctness of concurrent system in scenario-based software engineering. Formal verification techniques such as model checking can automatically check the consistence between the system and the properties. These properties are usually represented by linear temporal logics. Unfortunately, the inherent complication of linear temporal logic formulas makes model checking difficult to apply widely in industry practice. Property sequence chart is a scenarios-based visual language, which can solve this problem; it not only has the ability of powerful expression and simplicity, but also can tackle the defaults of currently used notations in industry such as UML 2.0 sequence diagrams and message sequence charts and, in academy, such as live sequence chart. In order to describe PSC clearly and make it used widely, this paper gives the formal syntax and formal semantic. The basic semantic of basic property sequence chart based on Büchi automaton is first given and then the semantic of how to get more complex property sequence chart with Par, Loop, Simulat operators is put forward. Semantic of how to compose two property sequence charts into a more complex one is also given. Finally, some examples are studied and its future applications in model checking are discussed.